0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 278 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 292 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPOrderProof (⇔, 757 ms)
↳22 QDP
↳23 PisEmptyProof (⇔, 0 ms)
↳24 YES
↳25 PiDP
↳26 UsableRulesProof (⇔, 0 ms)
↳27 PiDP
↳28 PiDPToQDPProof (⇒, 0 ms)
↳29 QDP
↳30 QDPOrderProof (⇔, 717 ms)
↳31 QDP
↳32 DependencyGraphProof (⇔, 1 ms)
↳33 TRUE
↳34 PiDP
↳35 UsableRulesProof (⇔, 1 ms)
↳36 PiDP
↳37 PiDPToQDPProof (⇒, 0 ms)
↳38 QDP
↳39 QDPOrderProof (⇔, 69 ms)
↳40 QDP
↳41 QDPOrderProof (⇔, 511 ms)
↳42 QDP
↳43 PisEmptyProof (⇔, 0 ms)
↳44 YES
cnfequivB_in_ga(n(n(T12)), T7) → U6_ga(T12, T7, cnfequivB_in_ga(T12, T7))
cnfequivB_in_ga(n(a(T23, T24)), T7) → U7_ga(T23, T24, T7, cnfequivB_in_ga(o(n(T23), n(T24)), T7))
cnfequivB_in_ga(n(o(T36, T37)), T7) → U8_ga(T36, T37, T7, cnfequivB_in_ga(a(n(T36), n(T37)), T7))
cnfequivB_in_ga(o(T53, a(T54, T55)), T7) → U9_ga(T53, T54, T55, T7, cnfequivB_in_ga(a(o(T53, T54), o(T53, T55)), T7))
cnfequivB_in_ga(o(a(T72, T73), T74), T7) → U10_ga(T72, T73, T74, T7, cnfequivB_in_ga(a(o(T72, T74), o(T73, T74)), T7))
cnfequivB_in_ga(o(T87, T88), T7) → U11_ga(T87, T88, T7, transformA_in_ga(T87, X97))
transformA_in_ga(n(n(T98)), T98) → transformA_out_ga(n(n(T98)), T98)
transformA_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transformA_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformA_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transformA_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformA_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transformA_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformA_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transformA_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformA_in_ga(o(T157, T158), o(X176, T158)) → U1_ga(T157, T158, X176, transformA_in_ga(T157, X176))
transformA_in_ga(o(T169, T170), o(T169, X198)) → U2_ga(T169, T170, X198, transformA_in_ga(T170, X198))
transformA_in_ga(a(T181, T182), a(X220, T182)) → U3_ga(T181, T182, X220, transformA_in_ga(T181, X220))
transformA_in_ga(a(T193, T194), a(T193, X242)) → U4_ga(T193, T194, X242, transformA_in_ga(T194, X242))
transformA_in_ga(n(T199), n(X253)) → U5_ga(T199, X253, transformA_in_ga(T199, X253))
U5_ga(T199, X253, transformA_out_ga(T199, X253)) → transformA_out_ga(n(T199), n(X253))
U4_ga(T193, T194, X242, transformA_out_ga(T194, X242)) → transformA_out_ga(a(T193, T194), a(T193, X242))
U3_ga(T181, T182, X220, transformA_out_ga(T181, X220)) → transformA_out_ga(a(T181, T182), a(X220, T182))
U2_ga(T169, T170, X198, transformA_out_ga(T170, X198)) → transformA_out_ga(o(T169, T170), o(T169, X198))
U1_ga(T157, T158, X176, transformA_out_ga(T157, X176)) → transformA_out_ga(o(T157, T158), o(X176, T158))
U11_ga(T87, T88, T7, transformA_out_ga(T87, X97)) → cnfequivB_out_ga(o(T87, T88), T7)
cnfequivB_in_ga(o(T87, T88), T7) → U12_ga(T87, T88, T7, transformA_in_ga(T87, T91))
U12_ga(T87, T88, T7, transformA_out_ga(T87, T91)) → U13_ga(T87, T88, T7, cnfequivB_in_ga(o(T91, T88), T7))
cnfequivB_in_ga(o(T213, T214), T7) → U14_ga(T213, T214, T7, transformA_in_ga(T214, X278))
U14_ga(T213, T214, T7, transformA_out_ga(T214, X278)) → cnfequivB_out_ga(o(T213, T214), T7)
cnfequivB_in_ga(o(T213, T214), T7) → U15_ga(T213, T214, T7, transformA_in_ga(T214, T217))
U15_ga(T213, T214, T7, transformA_out_ga(T214, T217)) → U16_ga(T213, T214, T7, cnfequivB_in_ga(o(T213, T217), T7))
cnfequivB_in_ga(a(T231, T232), T7) → U17_ga(T231, T232, T7, transformA_in_ga(T231, X305))
U17_ga(T231, T232, T7, transformA_out_ga(T231, X305)) → cnfequivB_out_ga(a(T231, T232), T7)
cnfequivB_in_ga(a(T231, T232), T7) → U18_ga(T231, T232, T7, transformA_in_ga(T231, T235))
U18_ga(T231, T232, T7, transformA_out_ga(T231, T235)) → U19_ga(T231, T232, T7, cnfequivB_in_ga(a(T235, T232), T7))
cnfequivB_in_ga(a(T249, T250), T7) → U20_ga(T249, T250, T7, transformA_in_ga(T250, X332))
U20_ga(T249, T250, T7, transformA_out_ga(T250, X332)) → cnfequivB_out_ga(a(T249, T250), T7)
cnfequivB_in_ga(a(T249, T250), T7) → U21_ga(T249, T250, T7, transformA_in_ga(T250, T253))
U21_ga(T249, T250, T7, transformA_out_ga(T250, T253)) → U22_ga(T249, T250, T7, cnfequivB_in_ga(a(T249, T253), T7))
cnfequivB_in_ga(n(T263), T7) → U23_ga(T263, T7, transformA_in_ga(T263, X354))
U23_ga(T263, T7, transformA_out_ga(T263, X354)) → cnfequivB_out_ga(n(T263), T7)
cnfequivB_in_ga(n(T263), T7) → U24_ga(T263, T7, transformA_in_ga(T263, T266))
U24_ga(T263, T7, transformA_out_ga(T263, T266)) → U25_ga(T263, T7, cnfequivB_in_ga(n(T266), T7))
cnfequivB_in_ga(T273, T273) → cnfequivB_out_ga(T273, T273)
U25_ga(T263, T7, cnfequivB_out_ga(n(T266), T7)) → cnfequivB_out_ga(n(T263), T7)
U22_ga(T249, T250, T7, cnfequivB_out_ga(a(T249, T253), T7)) → cnfequivB_out_ga(a(T249, T250), T7)
U19_ga(T231, T232, T7, cnfequivB_out_ga(a(T235, T232), T7)) → cnfequivB_out_ga(a(T231, T232), T7)
U16_ga(T213, T214, T7, cnfequivB_out_ga(o(T213, T217), T7)) → cnfequivB_out_ga(o(T213, T214), T7)
U13_ga(T87, T88, T7, cnfequivB_out_ga(o(T91, T88), T7)) → cnfequivB_out_ga(o(T87, T88), T7)
U10_ga(T72, T73, T74, T7, cnfequivB_out_ga(a(o(T72, T74), o(T73, T74)), T7)) → cnfequivB_out_ga(o(a(T72, T73), T74), T7)
U9_ga(T53, T54, T55, T7, cnfequivB_out_ga(a(o(T53, T54), o(T53, T55)), T7)) → cnfequivB_out_ga(o(T53, a(T54, T55)), T7)
U8_ga(T36, T37, T7, cnfequivB_out_ga(a(n(T36), n(T37)), T7)) → cnfequivB_out_ga(n(o(T36, T37)), T7)
U7_ga(T23, T24, T7, cnfequivB_out_ga(o(n(T23), n(T24)), T7)) → cnfequivB_out_ga(n(a(T23, T24)), T7)
U6_ga(T12, T7, cnfequivB_out_ga(T12, T7)) → cnfequivB_out_ga(n(n(T12)), T7)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
cnfequivB_in_ga(n(n(T12)), T7) → U6_ga(T12, T7, cnfequivB_in_ga(T12, T7))
cnfequivB_in_ga(n(a(T23, T24)), T7) → U7_ga(T23, T24, T7, cnfequivB_in_ga(o(n(T23), n(T24)), T7))
cnfequivB_in_ga(n(o(T36, T37)), T7) → U8_ga(T36, T37, T7, cnfequivB_in_ga(a(n(T36), n(T37)), T7))
cnfequivB_in_ga(o(T53, a(T54, T55)), T7) → U9_ga(T53, T54, T55, T7, cnfequivB_in_ga(a(o(T53, T54), o(T53, T55)), T7))
cnfequivB_in_ga(o(a(T72, T73), T74), T7) → U10_ga(T72, T73, T74, T7, cnfequivB_in_ga(a(o(T72, T74), o(T73, T74)), T7))
cnfequivB_in_ga(o(T87, T88), T7) → U11_ga(T87, T88, T7, transformA_in_ga(T87, X97))
transformA_in_ga(n(n(T98)), T98) → transformA_out_ga(n(n(T98)), T98)
transformA_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transformA_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformA_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transformA_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformA_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transformA_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformA_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transformA_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformA_in_ga(o(T157, T158), o(X176, T158)) → U1_ga(T157, T158, X176, transformA_in_ga(T157, X176))
transformA_in_ga(o(T169, T170), o(T169, X198)) → U2_ga(T169, T170, X198, transformA_in_ga(T170, X198))
transformA_in_ga(a(T181, T182), a(X220, T182)) → U3_ga(T181, T182, X220, transformA_in_ga(T181, X220))
transformA_in_ga(a(T193, T194), a(T193, X242)) → U4_ga(T193, T194, X242, transformA_in_ga(T194, X242))
transformA_in_ga(n(T199), n(X253)) → U5_ga(T199, X253, transformA_in_ga(T199, X253))
U5_ga(T199, X253, transformA_out_ga(T199, X253)) → transformA_out_ga(n(T199), n(X253))
U4_ga(T193, T194, X242, transformA_out_ga(T194, X242)) → transformA_out_ga(a(T193, T194), a(T193, X242))
U3_ga(T181, T182, X220, transformA_out_ga(T181, X220)) → transformA_out_ga(a(T181, T182), a(X220, T182))
U2_ga(T169, T170, X198, transformA_out_ga(T170, X198)) → transformA_out_ga(o(T169, T170), o(T169, X198))
U1_ga(T157, T158, X176, transformA_out_ga(T157, X176)) → transformA_out_ga(o(T157, T158), o(X176, T158))
U11_ga(T87, T88, T7, transformA_out_ga(T87, X97)) → cnfequivB_out_ga(o(T87, T88), T7)
cnfequivB_in_ga(o(T87, T88), T7) → U12_ga(T87, T88, T7, transformA_in_ga(T87, T91))
U12_ga(T87, T88, T7, transformA_out_ga(T87, T91)) → U13_ga(T87, T88, T7, cnfequivB_in_ga(o(T91, T88), T7))
cnfequivB_in_ga(o(T213, T214), T7) → U14_ga(T213, T214, T7, transformA_in_ga(T214, X278))
U14_ga(T213, T214, T7, transformA_out_ga(T214, X278)) → cnfequivB_out_ga(o(T213, T214), T7)
cnfequivB_in_ga(o(T213, T214), T7) → U15_ga(T213, T214, T7, transformA_in_ga(T214, T217))
U15_ga(T213, T214, T7, transformA_out_ga(T214, T217)) → U16_ga(T213, T214, T7, cnfequivB_in_ga(o(T213, T217), T7))
cnfequivB_in_ga(a(T231, T232), T7) → U17_ga(T231, T232, T7, transformA_in_ga(T231, X305))
U17_ga(T231, T232, T7, transformA_out_ga(T231, X305)) → cnfequivB_out_ga(a(T231, T232), T7)
cnfequivB_in_ga(a(T231, T232), T7) → U18_ga(T231, T232, T7, transformA_in_ga(T231, T235))
U18_ga(T231, T232, T7, transformA_out_ga(T231, T235)) → U19_ga(T231, T232, T7, cnfequivB_in_ga(a(T235, T232), T7))
cnfequivB_in_ga(a(T249, T250), T7) → U20_ga(T249, T250, T7, transformA_in_ga(T250, X332))
U20_ga(T249, T250, T7, transformA_out_ga(T250, X332)) → cnfequivB_out_ga(a(T249, T250), T7)
cnfequivB_in_ga(a(T249, T250), T7) → U21_ga(T249, T250, T7, transformA_in_ga(T250, T253))
U21_ga(T249, T250, T7, transformA_out_ga(T250, T253)) → U22_ga(T249, T250, T7, cnfequivB_in_ga(a(T249, T253), T7))
cnfequivB_in_ga(n(T263), T7) → U23_ga(T263, T7, transformA_in_ga(T263, X354))
U23_ga(T263, T7, transformA_out_ga(T263, X354)) → cnfequivB_out_ga(n(T263), T7)
cnfequivB_in_ga(n(T263), T7) → U24_ga(T263, T7, transformA_in_ga(T263, T266))
U24_ga(T263, T7, transformA_out_ga(T263, T266)) → U25_ga(T263, T7, cnfequivB_in_ga(n(T266), T7))
cnfequivB_in_ga(T273, T273) → cnfequivB_out_ga(T273, T273)
U25_ga(T263, T7, cnfequivB_out_ga(n(T266), T7)) → cnfequivB_out_ga(n(T263), T7)
U22_ga(T249, T250, T7, cnfequivB_out_ga(a(T249, T253), T7)) → cnfequivB_out_ga(a(T249, T250), T7)
U19_ga(T231, T232, T7, cnfequivB_out_ga(a(T235, T232), T7)) → cnfequivB_out_ga(a(T231, T232), T7)
U16_ga(T213, T214, T7, cnfequivB_out_ga(o(T213, T217), T7)) → cnfequivB_out_ga(o(T213, T214), T7)
U13_ga(T87, T88, T7, cnfequivB_out_ga(o(T91, T88), T7)) → cnfequivB_out_ga(o(T87, T88), T7)
U10_ga(T72, T73, T74, T7, cnfequivB_out_ga(a(o(T72, T74), o(T73, T74)), T7)) → cnfequivB_out_ga(o(a(T72, T73), T74), T7)
U9_ga(T53, T54, T55, T7, cnfequivB_out_ga(a(o(T53, T54), o(T53, T55)), T7)) → cnfequivB_out_ga(o(T53, a(T54, T55)), T7)
U8_ga(T36, T37, T7, cnfequivB_out_ga(a(n(T36), n(T37)), T7)) → cnfequivB_out_ga(n(o(T36, T37)), T7)
U7_ga(T23, T24, T7, cnfequivB_out_ga(o(n(T23), n(T24)), T7)) → cnfequivB_out_ga(n(a(T23, T24)), T7)
U6_ga(T12, T7, cnfequivB_out_ga(T12, T7)) → cnfequivB_out_ga(n(n(T12)), T7)
CNFEQUIVB_IN_GA(n(n(T12)), T7) → U6_GA(T12, T7, cnfequivB_in_ga(T12, T7))
CNFEQUIVB_IN_GA(n(n(T12)), T7) → CNFEQUIVB_IN_GA(T12, T7)
CNFEQUIVB_IN_GA(n(a(T23, T24)), T7) → U7_GA(T23, T24, T7, cnfequivB_in_ga(o(n(T23), n(T24)), T7))
CNFEQUIVB_IN_GA(n(a(T23, T24)), T7) → CNFEQUIVB_IN_GA(o(n(T23), n(T24)), T7)
CNFEQUIVB_IN_GA(n(o(T36, T37)), T7) → U8_GA(T36, T37, T7, cnfequivB_in_ga(a(n(T36), n(T37)), T7))
CNFEQUIVB_IN_GA(n(o(T36, T37)), T7) → CNFEQUIVB_IN_GA(a(n(T36), n(T37)), T7)
CNFEQUIVB_IN_GA(o(T53, a(T54, T55)), T7) → U9_GA(T53, T54, T55, T7, cnfequivB_in_ga(a(o(T53, T54), o(T53, T55)), T7))
CNFEQUIVB_IN_GA(o(T53, a(T54, T55)), T7) → CNFEQUIVB_IN_GA(a(o(T53, T54), o(T53, T55)), T7)
CNFEQUIVB_IN_GA(o(a(T72, T73), T74), T7) → U10_GA(T72, T73, T74, T7, cnfequivB_in_ga(a(o(T72, T74), o(T73, T74)), T7))
CNFEQUIVB_IN_GA(o(a(T72, T73), T74), T7) → CNFEQUIVB_IN_GA(a(o(T72, T74), o(T73, T74)), T7)
CNFEQUIVB_IN_GA(o(T87, T88), T7) → U11_GA(T87, T88, T7, transformA_in_ga(T87, X97))
CNFEQUIVB_IN_GA(o(T87, T88), T7) → TRANSFORMA_IN_GA(T87, X97)
TRANSFORMA_IN_GA(o(T157, T158), o(X176, T158)) → U1_GA(T157, T158, X176, transformA_in_ga(T157, X176))
TRANSFORMA_IN_GA(o(T157, T158), o(X176, T158)) → TRANSFORMA_IN_GA(T157, X176)
TRANSFORMA_IN_GA(o(T169, T170), o(T169, X198)) → U2_GA(T169, T170, X198, transformA_in_ga(T170, X198))
TRANSFORMA_IN_GA(o(T169, T170), o(T169, X198)) → TRANSFORMA_IN_GA(T170, X198)
TRANSFORMA_IN_GA(a(T181, T182), a(X220, T182)) → U3_GA(T181, T182, X220, transformA_in_ga(T181, X220))
TRANSFORMA_IN_GA(a(T181, T182), a(X220, T182)) → TRANSFORMA_IN_GA(T181, X220)
TRANSFORMA_IN_GA(a(T193, T194), a(T193, X242)) → U4_GA(T193, T194, X242, transformA_in_ga(T194, X242))
TRANSFORMA_IN_GA(a(T193, T194), a(T193, X242)) → TRANSFORMA_IN_GA(T194, X242)
TRANSFORMA_IN_GA(n(T199), n(X253)) → U5_GA(T199, X253, transformA_in_ga(T199, X253))
TRANSFORMA_IN_GA(n(T199), n(X253)) → TRANSFORMA_IN_GA(T199, X253)
CNFEQUIVB_IN_GA(o(T87, T88), T7) → U12_GA(T87, T88, T7, transformA_in_ga(T87, T91))
U12_GA(T87, T88, T7, transformA_out_ga(T87, T91)) → U13_GA(T87, T88, T7, cnfequivB_in_ga(o(T91, T88), T7))
U12_GA(T87, T88, T7, transformA_out_ga(T87, T91)) → CNFEQUIVB_IN_GA(o(T91, T88), T7)
CNFEQUIVB_IN_GA(o(T213, T214), T7) → U14_GA(T213, T214, T7, transformA_in_ga(T214, X278))
CNFEQUIVB_IN_GA(o(T213, T214), T7) → TRANSFORMA_IN_GA(T214, X278)
CNFEQUIVB_IN_GA(o(T213, T214), T7) → U15_GA(T213, T214, T7, transformA_in_ga(T214, T217))
U15_GA(T213, T214, T7, transformA_out_ga(T214, T217)) → U16_GA(T213, T214, T7, cnfequivB_in_ga(o(T213, T217), T7))
U15_GA(T213, T214, T7, transformA_out_ga(T214, T217)) → CNFEQUIVB_IN_GA(o(T213, T217), T7)
CNFEQUIVB_IN_GA(a(T231, T232), T7) → U17_GA(T231, T232, T7, transformA_in_ga(T231, X305))
CNFEQUIVB_IN_GA(a(T231, T232), T7) → TRANSFORMA_IN_GA(T231, X305)
CNFEQUIVB_IN_GA(a(T231, T232), T7) → U18_GA(T231, T232, T7, transformA_in_ga(T231, T235))
U18_GA(T231, T232, T7, transformA_out_ga(T231, T235)) → U19_GA(T231, T232, T7, cnfequivB_in_ga(a(T235, T232), T7))
U18_GA(T231, T232, T7, transformA_out_ga(T231, T235)) → CNFEQUIVB_IN_GA(a(T235, T232), T7)
CNFEQUIVB_IN_GA(a(T249, T250), T7) → U20_GA(T249, T250, T7, transformA_in_ga(T250, X332))
CNFEQUIVB_IN_GA(a(T249, T250), T7) → TRANSFORMA_IN_GA(T250, X332)
CNFEQUIVB_IN_GA(a(T249, T250), T7) → U21_GA(T249, T250, T7, transformA_in_ga(T250, T253))
U21_GA(T249, T250, T7, transformA_out_ga(T250, T253)) → U22_GA(T249, T250, T7, cnfequivB_in_ga(a(T249, T253), T7))
U21_GA(T249, T250, T7, transformA_out_ga(T250, T253)) → CNFEQUIVB_IN_GA(a(T249, T253), T7)
CNFEQUIVB_IN_GA(n(T263), T7) → U23_GA(T263, T7, transformA_in_ga(T263, X354))
CNFEQUIVB_IN_GA(n(T263), T7) → TRANSFORMA_IN_GA(T263, X354)
CNFEQUIVB_IN_GA(n(T263), T7) → U24_GA(T263, T7, transformA_in_ga(T263, T266))
U24_GA(T263, T7, transformA_out_ga(T263, T266)) → U25_GA(T263, T7, cnfequivB_in_ga(n(T266), T7))
U24_GA(T263, T7, transformA_out_ga(T263, T266)) → CNFEQUIVB_IN_GA(n(T266), T7)
cnfequivB_in_ga(n(n(T12)), T7) → U6_ga(T12, T7, cnfequivB_in_ga(T12, T7))
cnfequivB_in_ga(n(a(T23, T24)), T7) → U7_ga(T23, T24, T7, cnfequivB_in_ga(o(n(T23), n(T24)), T7))
cnfequivB_in_ga(n(o(T36, T37)), T7) → U8_ga(T36, T37, T7, cnfequivB_in_ga(a(n(T36), n(T37)), T7))
cnfequivB_in_ga(o(T53, a(T54, T55)), T7) → U9_ga(T53, T54, T55, T7, cnfequivB_in_ga(a(o(T53, T54), o(T53, T55)), T7))
cnfequivB_in_ga(o(a(T72, T73), T74), T7) → U10_ga(T72, T73, T74, T7, cnfequivB_in_ga(a(o(T72, T74), o(T73, T74)), T7))
cnfequivB_in_ga(o(T87, T88), T7) → U11_ga(T87, T88, T7, transformA_in_ga(T87, X97))
transformA_in_ga(n(n(T98)), T98) → transformA_out_ga(n(n(T98)), T98)
transformA_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transformA_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformA_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transformA_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformA_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transformA_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformA_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transformA_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformA_in_ga(o(T157, T158), o(X176, T158)) → U1_ga(T157, T158, X176, transformA_in_ga(T157, X176))
transformA_in_ga(o(T169, T170), o(T169, X198)) → U2_ga(T169, T170, X198, transformA_in_ga(T170, X198))
transformA_in_ga(a(T181, T182), a(X220, T182)) → U3_ga(T181, T182, X220, transformA_in_ga(T181, X220))
transformA_in_ga(a(T193, T194), a(T193, X242)) → U4_ga(T193, T194, X242, transformA_in_ga(T194, X242))
transformA_in_ga(n(T199), n(X253)) → U5_ga(T199, X253, transformA_in_ga(T199, X253))
U5_ga(T199, X253, transformA_out_ga(T199, X253)) → transformA_out_ga(n(T199), n(X253))
U4_ga(T193, T194, X242, transformA_out_ga(T194, X242)) → transformA_out_ga(a(T193, T194), a(T193, X242))
U3_ga(T181, T182, X220, transformA_out_ga(T181, X220)) → transformA_out_ga(a(T181, T182), a(X220, T182))
U2_ga(T169, T170, X198, transformA_out_ga(T170, X198)) → transformA_out_ga(o(T169, T170), o(T169, X198))
U1_ga(T157, T158, X176, transformA_out_ga(T157, X176)) → transformA_out_ga(o(T157, T158), o(X176, T158))
U11_ga(T87, T88, T7, transformA_out_ga(T87, X97)) → cnfequivB_out_ga(o(T87, T88), T7)
cnfequivB_in_ga(o(T87, T88), T7) → U12_ga(T87, T88, T7, transformA_in_ga(T87, T91))
U12_ga(T87, T88, T7, transformA_out_ga(T87, T91)) → U13_ga(T87, T88, T7, cnfequivB_in_ga(o(T91, T88), T7))
cnfequivB_in_ga(o(T213, T214), T7) → U14_ga(T213, T214, T7, transformA_in_ga(T214, X278))
U14_ga(T213, T214, T7, transformA_out_ga(T214, X278)) → cnfequivB_out_ga(o(T213, T214), T7)
cnfequivB_in_ga(o(T213, T214), T7) → U15_ga(T213, T214, T7, transformA_in_ga(T214, T217))
U15_ga(T213, T214, T7, transformA_out_ga(T214, T217)) → U16_ga(T213, T214, T7, cnfequivB_in_ga(o(T213, T217), T7))
cnfequivB_in_ga(a(T231, T232), T7) → U17_ga(T231, T232, T7, transformA_in_ga(T231, X305))
U17_ga(T231, T232, T7, transformA_out_ga(T231, X305)) → cnfequivB_out_ga(a(T231, T232), T7)
cnfequivB_in_ga(a(T231, T232), T7) → U18_ga(T231, T232, T7, transformA_in_ga(T231, T235))
U18_ga(T231, T232, T7, transformA_out_ga(T231, T235)) → U19_ga(T231, T232, T7, cnfequivB_in_ga(a(T235, T232), T7))
cnfequivB_in_ga(a(T249, T250), T7) → U20_ga(T249, T250, T7, transformA_in_ga(T250, X332))
U20_ga(T249, T250, T7, transformA_out_ga(T250, X332)) → cnfequivB_out_ga(a(T249, T250), T7)
cnfequivB_in_ga(a(T249, T250), T7) → U21_ga(T249, T250, T7, transformA_in_ga(T250, T253))
U21_ga(T249, T250, T7, transformA_out_ga(T250, T253)) → U22_ga(T249, T250, T7, cnfequivB_in_ga(a(T249, T253), T7))
cnfequivB_in_ga(n(T263), T7) → U23_ga(T263, T7, transformA_in_ga(T263, X354))
U23_ga(T263, T7, transformA_out_ga(T263, X354)) → cnfequivB_out_ga(n(T263), T7)
cnfequivB_in_ga(n(T263), T7) → U24_ga(T263, T7, transformA_in_ga(T263, T266))
U24_ga(T263, T7, transformA_out_ga(T263, T266)) → U25_ga(T263, T7, cnfequivB_in_ga(n(T266), T7))
cnfequivB_in_ga(T273, T273) → cnfequivB_out_ga(T273, T273)
U25_ga(T263, T7, cnfequivB_out_ga(n(T266), T7)) → cnfequivB_out_ga(n(T263), T7)
U22_ga(T249, T250, T7, cnfequivB_out_ga(a(T249, T253), T7)) → cnfequivB_out_ga(a(T249, T250), T7)
U19_ga(T231, T232, T7, cnfequivB_out_ga(a(T235, T232), T7)) → cnfequivB_out_ga(a(T231, T232), T7)
U16_ga(T213, T214, T7, cnfequivB_out_ga(o(T213, T217), T7)) → cnfequivB_out_ga(o(T213, T214), T7)
U13_ga(T87, T88, T7, cnfequivB_out_ga(o(T91, T88), T7)) → cnfequivB_out_ga(o(T87, T88), T7)
U10_ga(T72, T73, T74, T7, cnfequivB_out_ga(a(o(T72, T74), o(T73, T74)), T7)) → cnfequivB_out_ga(o(a(T72, T73), T74), T7)
U9_ga(T53, T54, T55, T7, cnfequivB_out_ga(a(o(T53, T54), o(T53, T55)), T7)) → cnfequivB_out_ga(o(T53, a(T54, T55)), T7)
U8_ga(T36, T37, T7, cnfequivB_out_ga(a(n(T36), n(T37)), T7)) → cnfequivB_out_ga(n(o(T36, T37)), T7)
U7_ga(T23, T24, T7, cnfequivB_out_ga(o(n(T23), n(T24)), T7)) → cnfequivB_out_ga(n(a(T23, T24)), T7)
U6_ga(T12, T7, cnfequivB_out_ga(T12, T7)) → cnfequivB_out_ga(n(n(T12)), T7)
CNFEQUIVB_IN_GA(n(n(T12)), T7) → U6_GA(T12, T7, cnfequivB_in_ga(T12, T7))
CNFEQUIVB_IN_GA(n(n(T12)), T7) → CNFEQUIVB_IN_GA(T12, T7)
CNFEQUIVB_IN_GA(n(a(T23, T24)), T7) → U7_GA(T23, T24, T7, cnfequivB_in_ga(o(n(T23), n(T24)), T7))
CNFEQUIVB_IN_GA(n(a(T23, T24)), T7) → CNFEQUIVB_IN_GA(o(n(T23), n(T24)), T7)
CNFEQUIVB_IN_GA(n(o(T36, T37)), T7) → U8_GA(T36, T37, T7, cnfequivB_in_ga(a(n(T36), n(T37)), T7))
CNFEQUIVB_IN_GA(n(o(T36, T37)), T7) → CNFEQUIVB_IN_GA(a(n(T36), n(T37)), T7)
CNFEQUIVB_IN_GA(o(T53, a(T54, T55)), T7) → U9_GA(T53, T54, T55, T7, cnfequivB_in_ga(a(o(T53, T54), o(T53, T55)), T7))
CNFEQUIVB_IN_GA(o(T53, a(T54, T55)), T7) → CNFEQUIVB_IN_GA(a(o(T53, T54), o(T53, T55)), T7)
CNFEQUIVB_IN_GA(o(a(T72, T73), T74), T7) → U10_GA(T72, T73, T74, T7, cnfequivB_in_ga(a(o(T72, T74), o(T73, T74)), T7))
CNFEQUIVB_IN_GA(o(a(T72, T73), T74), T7) → CNFEQUIVB_IN_GA(a(o(T72, T74), o(T73, T74)), T7)
CNFEQUIVB_IN_GA(o(T87, T88), T7) → U11_GA(T87, T88, T7, transformA_in_ga(T87, X97))
CNFEQUIVB_IN_GA(o(T87, T88), T7) → TRANSFORMA_IN_GA(T87, X97)
TRANSFORMA_IN_GA(o(T157, T158), o(X176, T158)) → U1_GA(T157, T158, X176, transformA_in_ga(T157, X176))
TRANSFORMA_IN_GA(o(T157, T158), o(X176, T158)) → TRANSFORMA_IN_GA(T157, X176)
TRANSFORMA_IN_GA(o(T169, T170), o(T169, X198)) → U2_GA(T169, T170, X198, transformA_in_ga(T170, X198))
TRANSFORMA_IN_GA(o(T169, T170), o(T169, X198)) → TRANSFORMA_IN_GA(T170, X198)
TRANSFORMA_IN_GA(a(T181, T182), a(X220, T182)) → U3_GA(T181, T182, X220, transformA_in_ga(T181, X220))
TRANSFORMA_IN_GA(a(T181, T182), a(X220, T182)) → TRANSFORMA_IN_GA(T181, X220)
TRANSFORMA_IN_GA(a(T193, T194), a(T193, X242)) → U4_GA(T193, T194, X242, transformA_in_ga(T194, X242))
TRANSFORMA_IN_GA(a(T193, T194), a(T193, X242)) → TRANSFORMA_IN_GA(T194, X242)
TRANSFORMA_IN_GA(n(T199), n(X253)) → U5_GA(T199, X253, transformA_in_ga(T199, X253))
TRANSFORMA_IN_GA(n(T199), n(X253)) → TRANSFORMA_IN_GA(T199, X253)
CNFEQUIVB_IN_GA(o(T87, T88), T7) → U12_GA(T87, T88, T7, transformA_in_ga(T87, T91))
U12_GA(T87, T88, T7, transformA_out_ga(T87, T91)) → U13_GA(T87, T88, T7, cnfequivB_in_ga(o(T91, T88), T7))
U12_GA(T87, T88, T7, transformA_out_ga(T87, T91)) → CNFEQUIVB_IN_GA(o(T91, T88), T7)
CNFEQUIVB_IN_GA(o(T213, T214), T7) → U14_GA(T213, T214, T7, transformA_in_ga(T214, X278))
CNFEQUIVB_IN_GA(o(T213, T214), T7) → TRANSFORMA_IN_GA(T214, X278)
CNFEQUIVB_IN_GA(o(T213, T214), T7) → U15_GA(T213, T214, T7, transformA_in_ga(T214, T217))
U15_GA(T213, T214, T7, transformA_out_ga(T214, T217)) → U16_GA(T213, T214, T7, cnfequivB_in_ga(o(T213, T217), T7))
U15_GA(T213, T214, T7, transformA_out_ga(T214, T217)) → CNFEQUIVB_IN_GA(o(T213, T217), T7)
CNFEQUIVB_IN_GA(a(T231, T232), T7) → U17_GA(T231, T232, T7, transformA_in_ga(T231, X305))
CNFEQUIVB_IN_GA(a(T231, T232), T7) → TRANSFORMA_IN_GA(T231, X305)
CNFEQUIVB_IN_GA(a(T231, T232), T7) → U18_GA(T231, T232, T7, transformA_in_ga(T231, T235))
U18_GA(T231, T232, T7, transformA_out_ga(T231, T235)) → U19_GA(T231, T232, T7, cnfequivB_in_ga(a(T235, T232), T7))
U18_GA(T231, T232, T7, transformA_out_ga(T231, T235)) → CNFEQUIVB_IN_GA(a(T235, T232), T7)
CNFEQUIVB_IN_GA(a(T249, T250), T7) → U20_GA(T249, T250, T7, transformA_in_ga(T250, X332))
CNFEQUIVB_IN_GA(a(T249, T250), T7) → TRANSFORMA_IN_GA(T250, X332)
CNFEQUIVB_IN_GA(a(T249, T250), T7) → U21_GA(T249, T250, T7, transformA_in_ga(T250, T253))
U21_GA(T249, T250, T7, transformA_out_ga(T250, T253)) → U22_GA(T249, T250, T7, cnfequivB_in_ga(a(T249, T253), T7))
U21_GA(T249, T250, T7, transformA_out_ga(T250, T253)) → CNFEQUIVB_IN_GA(a(T249, T253), T7)
CNFEQUIVB_IN_GA(n(T263), T7) → U23_GA(T263, T7, transformA_in_ga(T263, X354))
CNFEQUIVB_IN_GA(n(T263), T7) → TRANSFORMA_IN_GA(T263, X354)
CNFEQUIVB_IN_GA(n(T263), T7) → U24_GA(T263, T7, transformA_in_ga(T263, T266))
U24_GA(T263, T7, transformA_out_ga(T263, T266)) → U25_GA(T263, T7, cnfequivB_in_ga(n(T266), T7))
U24_GA(T263, T7, transformA_out_ga(T263, T266)) → CNFEQUIVB_IN_GA(n(T266), T7)
cnfequivB_in_ga(n(n(T12)), T7) → U6_ga(T12, T7, cnfequivB_in_ga(T12, T7))
cnfequivB_in_ga(n(a(T23, T24)), T7) → U7_ga(T23, T24, T7, cnfequivB_in_ga(o(n(T23), n(T24)), T7))
cnfequivB_in_ga(n(o(T36, T37)), T7) → U8_ga(T36, T37, T7, cnfequivB_in_ga(a(n(T36), n(T37)), T7))
cnfequivB_in_ga(o(T53, a(T54, T55)), T7) → U9_ga(T53, T54, T55, T7, cnfequivB_in_ga(a(o(T53, T54), o(T53, T55)), T7))
cnfequivB_in_ga(o(a(T72, T73), T74), T7) → U10_ga(T72, T73, T74, T7, cnfequivB_in_ga(a(o(T72, T74), o(T73, T74)), T7))
cnfequivB_in_ga(o(T87, T88), T7) → U11_ga(T87, T88, T7, transformA_in_ga(T87, X97))
transformA_in_ga(n(n(T98)), T98) → transformA_out_ga(n(n(T98)), T98)
transformA_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transformA_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformA_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transformA_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformA_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transformA_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformA_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transformA_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformA_in_ga(o(T157, T158), o(X176, T158)) → U1_ga(T157, T158, X176, transformA_in_ga(T157, X176))
transformA_in_ga(o(T169, T170), o(T169, X198)) → U2_ga(T169, T170, X198, transformA_in_ga(T170, X198))
transformA_in_ga(a(T181, T182), a(X220, T182)) → U3_ga(T181, T182, X220, transformA_in_ga(T181, X220))
transformA_in_ga(a(T193, T194), a(T193, X242)) → U4_ga(T193, T194, X242, transformA_in_ga(T194, X242))
transformA_in_ga(n(T199), n(X253)) → U5_ga(T199, X253, transformA_in_ga(T199, X253))
U5_ga(T199, X253, transformA_out_ga(T199, X253)) → transformA_out_ga(n(T199), n(X253))
U4_ga(T193, T194, X242, transformA_out_ga(T194, X242)) → transformA_out_ga(a(T193, T194), a(T193, X242))
U3_ga(T181, T182, X220, transformA_out_ga(T181, X220)) → transformA_out_ga(a(T181, T182), a(X220, T182))
U2_ga(T169, T170, X198, transformA_out_ga(T170, X198)) → transformA_out_ga(o(T169, T170), o(T169, X198))
U1_ga(T157, T158, X176, transformA_out_ga(T157, X176)) → transformA_out_ga(o(T157, T158), o(X176, T158))
U11_ga(T87, T88, T7, transformA_out_ga(T87, X97)) → cnfequivB_out_ga(o(T87, T88), T7)
cnfequivB_in_ga(o(T87, T88), T7) → U12_ga(T87, T88, T7, transformA_in_ga(T87, T91))
U12_ga(T87, T88, T7, transformA_out_ga(T87, T91)) → U13_ga(T87, T88, T7, cnfequivB_in_ga(o(T91, T88), T7))
cnfequivB_in_ga(o(T213, T214), T7) → U14_ga(T213, T214, T7, transformA_in_ga(T214, X278))
U14_ga(T213, T214, T7, transformA_out_ga(T214, X278)) → cnfequivB_out_ga(o(T213, T214), T7)
cnfequivB_in_ga(o(T213, T214), T7) → U15_ga(T213, T214, T7, transformA_in_ga(T214, T217))
U15_ga(T213, T214, T7, transformA_out_ga(T214, T217)) → U16_ga(T213, T214, T7, cnfequivB_in_ga(o(T213, T217), T7))
cnfequivB_in_ga(a(T231, T232), T7) → U17_ga(T231, T232, T7, transformA_in_ga(T231, X305))
U17_ga(T231, T232, T7, transformA_out_ga(T231, X305)) → cnfequivB_out_ga(a(T231, T232), T7)
cnfequivB_in_ga(a(T231, T232), T7) → U18_ga(T231, T232, T7, transformA_in_ga(T231, T235))
U18_ga(T231, T232, T7, transformA_out_ga(T231, T235)) → U19_ga(T231, T232, T7, cnfequivB_in_ga(a(T235, T232), T7))
cnfequivB_in_ga(a(T249, T250), T7) → U20_ga(T249, T250, T7, transformA_in_ga(T250, X332))
U20_ga(T249, T250, T7, transformA_out_ga(T250, X332)) → cnfequivB_out_ga(a(T249, T250), T7)
cnfequivB_in_ga(a(T249, T250), T7) → U21_ga(T249, T250, T7, transformA_in_ga(T250, T253))
U21_ga(T249, T250, T7, transformA_out_ga(T250, T253)) → U22_ga(T249, T250, T7, cnfequivB_in_ga(a(T249, T253), T7))
cnfequivB_in_ga(n(T263), T7) → U23_ga(T263, T7, transformA_in_ga(T263, X354))
U23_ga(T263, T7, transformA_out_ga(T263, X354)) → cnfequivB_out_ga(n(T263), T7)
cnfequivB_in_ga(n(T263), T7) → U24_ga(T263, T7, transformA_in_ga(T263, T266))
U24_ga(T263, T7, transformA_out_ga(T263, T266)) → U25_ga(T263, T7, cnfequivB_in_ga(n(T266), T7))
cnfequivB_in_ga(T273, T273) → cnfequivB_out_ga(T273, T273)
U25_ga(T263, T7, cnfequivB_out_ga(n(T266), T7)) → cnfequivB_out_ga(n(T263), T7)
U22_ga(T249, T250, T7, cnfequivB_out_ga(a(T249, T253), T7)) → cnfequivB_out_ga(a(T249, T250), T7)
U19_ga(T231, T232, T7, cnfequivB_out_ga(a(T235, T232), T7)) → cnfequivB_out_ga(a(T231, T232), T7)
U16_ga(T213, T214, T7, cnfequivB_out_ga(o(T213, T217), T7)) → cnfequivB_out_ga(o(T213, T214), T7)
U13_ga(T87, T88, T7, cnfequivB_out_ga(o(T91, T88), T7)) → cnfequivB_out_ga(o(T87, T88), T7)
U10_ga(T72, T73, T74, T7, cnfequivB_out_ga(a(o(T72, T74), o(T73, T74)), T7)) → cnfequivB_out_ga(o(a(T72, T73), T74), T7)
U9_ga(T53, T54, T55, T7, cnfequivB_out_ga(a(o(T53, T54), o(T53, T55)), T7)) → cnfequivB_out_ga(o(T53, a(T54, T55)), T7)
U8_ga(T36, T37, T7, cnfequivB_out_ga(a(n(T36), n(T37)), T7)) → cnfequivB_out_ga(n(o(T36, T37)), T7)
U7_ga(T23, T24, T7, cnfequivB_out_ga(o(n(T23), n(T24)), T7)) → cnfequivB_out_ga(n(a(T23, T24)), T7)
U6_ga(T12, T7, cnfequivB_out_ga(T12, T7)) → cnfequivB_out_ga(n(n(T12)), T7)
TRANSFORMA_IN_GA(o(T169, T170), o(T169, X198)) → TRANSFORMA_IN_GA(T170, X198)
TRANSFORMA_IN_GA(o(T157, T158), o(X176, T158)) → TRANSFORMA_IN_GA(T157, X176)
TRANSFORMA_IN_GA(a(T181, T182), a(X220, T182)) → TRANSFORMA_IN_GA(T181, X220)
TRANSFORMA_IN_GA(a(T193, T194), a(T193, X242)) → TRANSFORMA_IN_GA(T194, X242)
TRANSFORMA_IN_GA(n(T199), n(X253)) → TRANSFORMA_IN_GA(T199, X253)
cnfequivB_in_ga(n(n(T12)), T7) → U6_ga(T12, T7, cnfequivB_in_ga(T12, T7))
cnfequivB_in_ga(n(a(T23, T24)), T7) → U7_ga(T23, T24, T7, cnfequivB_in_ga(o(n(T23), n(T24)), T7))
cnfequivB_in_ga(n(o(T36, T37)), T7) → U8_ga(T36, T37, T7, cnfequivB_in_ga(a(n(T36), n(T37)), T7))
cnfequivB_in_ga(o(T53, a(T54, T55)), T7) → U9_ga(T53, T54, T55, T7, cnfequivB_in_ga(a(o(T53, T54), o(T53, T55)), T7))
cnfequivB_in_ga(o(a(T72, T73), T74), T7) → U10_ga(T72, T73, T74, T7, cnfequivB_in_ga(a(o(T72, T74), o(T73, T74)), T7))
cnfequivB_in_ga(o(T87, T88), T7) → U11_ga(T87, T88, T7, transformA_in_ga(T87, X97))
transformA_in_ga(n(n(T98)), T98) → transformA_out_ga(n(n(T98)), T98)
transformA_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transformA_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformA_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transformA_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformA_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transformA_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformA_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transformA_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformA_in_ga(o(T157, T158), o(X176, T158)) → U1_ga(T157, T158, X176, transformA_in_ga(T157, X176))
transformA_in_ga(o(T169, T170), o(T169, X198)) → U2_ga(T169, T170, X198, transformA_in_ga(T170, X198))
transformA_in_ga(a(T181, T182), a(X220, T182)) → U3_ga(T181, T182, X220, transformA_in_ga(T181, X220))
transformA_in_ga(a(T193, T194), a(T193, X242)) → U4_ga(T193, T194, X242, transformA_in_ga(T194, X242))
transformA_in_ga(n(T199), n(X253)) → U5_ga(T199, X253, transformA_in_ga(T199, X253))
U5_ga(T199, X253, transformA_out_ga(T199, X253)) → transformA_out_ga(n(T199), n(X253))
U4_ga(T193, T194, X242, transformA_out_ga(T194, X242)) → transformA_out_ga(a(T193, T194), a(T193, X242))
U3_ga(T181, T182, X220, transformA_out_ga(T181, X220)) → transformA_out_ga(a(T181, T182), a(X220, T182))
U2_ga(T169, T170, X198, transformA_out_ga(T170, X198)) → transformA_out_ga(o(T169, T170), o(T169, X198))
U1_ga(T157, T158, X176, transformA_out_ga(T157, X176)) → transformA_out_ga(o(T157, T158), o(X176, T158))
U11_ga(T87, T88, T7, transformA_out_ga(T87, X97)) → cnfequivB_out_ga(o(T87, T88), T7)
cnfequivB_in_ga(o(T87, T88), T7) → U12_ga(T87, T88, T7, transformA_in_ga(T87, T91))
U12_ga(T87, T88, T7, transformA_out_ga(T87, T91)) → U13_ga(T87, T88, T7, cnfequivB_in_ga(o(T91, T88), T7))
cnfequivB_in_ga(o(T213, T214), T7) → U14_ga(T213, T214, T7, transformA_in_ga(T214, X278))
U14_ga(T213, T214, T7, transformA_out_ga(T214, X278)) → cnfequivB_out_ga(o(T213, T214), T7)
cnfequivB_in_ga(o(T213, T214), T7) → U15_ga(T213, T214, T7, transformA_in_ga(T214, T217))
U15_ga(T213, T214, T7, transformA_out_ga(T214, T217)) → U16_ga(T213, T214, T7, cnfequivB_in_ga(o(T213, T217), T7))
cnfequivB_in_ga(a(T231, T232), T7) → U17_ga(T231, T232, T7, transformA_in_ga(T231, X305))
U17_ga(T231, T232, T7, transformA_out_ga(T231, X305)) → cnfequivB_out_ga(a(T231, T232), T7)
cnfequivB_in_ga(a(T231, T232), T7) → U18_ga(T231, T232, T7, transformA_in_ga(T231, T235))
U18_ga(T231, T232, T7, transformA_out_ga(T231, T235)) → U19_ga(T231, T232, T7, cnfequivB_in_ga(a(T235, T232), T7))
cnfequivB_in_ga(a(T249, T250), T7) → U20_ga(T249, T250, T7, transformA_in_ga(T250, X332))
U20_ga(T249, T250, T7, transformA_out_ga(T250, X332)) → cnfequivB_out_ga(a(T249, T250), T7)
cnfequivB_in_ga(a(T249, T250), T7) → U21_ga(T249, T250, T7, transformA_in_ga(T250, T253))
U21_ga(T249, T250, T7, transformA_out_ga(T250, T253)) → U22_ga(T249, T250, T7, cnfequivB_in_ga(a(T249, T253), T7))
cnfequivB_in_ga(n(T263), T7) → U23_ga(T263, T7, transformA_in_ga(T263, X354))
U23_ga(T263, T7, transformA_out_ga(T263, X354)) → cnfequivB_out_ga(n(T263), T7)
cnfequivB_in_ga(n(T263), T7) → U24_ga(T263, T7, transformA_in_ga(T263, T266))
U24_ga(T263, T7, transformA_out_ga(T263, T266)) → U25_ga(T263, T7, cnfequivB_in_ga(n(T266), T7))
cnfequivB_in_ga(T273, T273) → cnfequivB_out_ga(T273, T273)
U25_ga(T263, T7, cnfequivB_out_ga(n(T266), T7)) → cnfequivB_out_ga(n(T263), T7)
U22_ga(T249, T250, T7, cnfequivB_out_ga(a(T249, T253), T7)) → cnfequivB_out_ga(a(T249, T250), T7)
U19_ga(T231, T232, T7, cnfequivB_out_ga(a(T235, T232), T7)) → cnfequivB_out_ga(a(T231, T232), T7)
U16_ga(T213, T214, T7, cnfequivB_out_ga(o(T213, T217), T7)) → cnfequivB_out_ga(o(T213, T214), T7)
U13_ga(T87, T88, T7, cnfequivB_out_ga(o(T91, T88), T7)) → cnfequivB_out_ga(o(T87, T88), T7)
U10_ga(T72, T73, T74, T7, cnfequivB_out_ga(a(o(T72, T74), o(T73, T74)), T7)) → cnfequivB_out_ga(o(a(T72, T73), T74), T7)
U9_ga(T53, T54, T55, T7, cnfequivB_out_ga(a(o(T53, T54), o(T53, T55)), T7)) → cnfequivB_out_ga(o(T53, a(T54, T55)), T7)
U8_ga(T36, T37, T7, cnfequivB_out_ga(a(n(T36), n(T37)), T7)) → cnfequivB_out_ga(n(o(T36, T37)), T7)
U7_ga(T23, T24, T7, cnfequivB_out_ga(o(n(T23), n(T24)), T7)) → cnfequivB_out_ga(n(a(T23, T24)), T7)
U6_ga(T12, T7, cnfequivB_out_ga(T12, T7)) → cnfequivB_out_ga(n(n(T12)), T7)
TRANSFORMA_IN_GA(o(T169, T170), o(T169, X198)) → TRANSFORMA_IN_GA(T170, X198)
TRANSFORMA_IN_GA(o(T157, T158), o(X176, T158)) → TRANSFORMA_IN_GA(T157, X176)
TRANSFORMA_IN_GA(a(T181, T182), a(X220, T182)) → TRANSFORMA_IN_GA(T181, X220)
TRANSFORMA_IN_GA(a(T193, T194), a(T193, X242)) → TRANSFORMA_IN_GA(T194, X242)
TRANSFORMA_IN_GA(n(T199), n(X253)) → TRANSFORMA_IN_GA(T199, X253)
TRANSFORMA_IN_GA(o(T169, T170)) → TRANSFORMA_IN_GA(T170)
TRANSFORMA_IN_GA(o(T157, T158)) → TRANSFORMA_IN_GA(T157)
TRANSFORMA_IN_GA(a(T181, T182)) → TRANSFORMA_IN_GA(T181)
TRANSFORMA_IN_GA(a(T193, T194)) → TRANSFORMA_IN_GA(T194)
TRANSFORMA_IN_GA(n(T199)) → TRANSFORMA_IN_GA(T199)
From the DPs we obtained the following set of size-change graphs:
CNFEQUIVB_IN_GA(a(T231, T232), T7) → U18_GA(T231, T232, T7, transformA_in_ga(T231, T235))
U18_GA(T231, T232, T7, transformA_out_ga(T231, T235)) → CNFEQUIVB_IN_GA(a(T235, T232), T7)
CNFEQUIVB_IN_GA(a(T249, T250), T7) → U21_GA(T249, T250, T7, transformA_in_ga(T250, T253))
U21_GA(T249, T250, T7, transformA_out_ga(T250, T253)) → CNFEQUIVB_IN_GA(a(T249, T253), T7)
cnfequivB_in_ga(n(n(T12)), T7) → U6_ga(T12, T7, cnfequivB_in_ga(T12, T7))
cnfequivB_in_ga(n(a(T23, T24)), T7) → U7_ga(T23, T24, T7, cnfequivB_in_ga(o(n(T23), n(T24)), T7))
cnfequivB_in_ga(n(o(T36, T37)), T7) → U8_ga(T36, T37, T7, cnfequivB_in_ga(a(n(T36), n(T37)), T7))
cnfequivB_in_ga(o(T53, a(T54, T55)), T7) → U9_ga(T53, T54, T55, T7, cnfequivB_in_ga(a(o(T53, T54), o(T53, T55)), T7))
cnfequivB_in_ga(o(a(T72, T73), T74), T7) → U10_ga(T72, T73, T74, T7, cnfequivB_in_ga(a(o(T72, T74), o(T73, T74)), T7))
cnfequivB_in_ga(o(T87, T88), T7) → U11_ga(T87, T88, T7, transformA_in_ga(T87, X97))
transformA_in_ga(n(n(T98)), T98) → transformA_out_ga(n(n(T98)), T98)
transformA_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transformA_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformA_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transformA_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformA_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transformA_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformA_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transformA_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformA_in_ga(o(T157, T158), o(X176, T158)) → U1_ga(T157, T158, X176, transformA_in_ga(T157, X176))
transformA_in_ga(o(T169, T170), o(T169, X198)) → U2_ga(T169, T170, X198, transformA_in_ga(T170, X198))
transformA_in_ga(a(T181, T182), a(X220, T182)) → U3_ga(T181, T182, X220, transformA_in_ga(T181, X220))
transformA_in_ga(a(T193, T194), a(T193, X242)) → U4_ga(T193, T194, X242, transformA_in_ga(T194, X242))
transformA_in_ga(n(T199), n(X253)) → U5_ga(T199, X253, transformA_in_ga(T199, X253))
U5_ga(T199, X253, transformA_out_ga(T199, X253)) → transformA_out_ga(n(T199), n(X253))
U4_ga(T193, T194, X242, transformA_out_ga(T194, X242)) → transformA_out_ga(a(T193, T194), a(T193, X242))
U3_ga(T181, T182, X220, transformA_out_ga(T181, X220)) → transformA_out_ga(a(T181, T182), a(X220, T182))
U2_ga(T169, T170, X198, transformA_out_ga(T170, X198)) → transformA_out_ga(o(T169, T170), o(T169, X198))
U1_ga(T157, T158, X176, transformA_out_ga(T157, X176)) → transformA_out_ga(o(T157, T158), o(X176, T158))
U11_ga(T87, T88, T7, transformA_out_ga(T87, X97)) → cnfequivB_out_ga(o(T87, T88), T7)
cnfequivB_in_ga(o(T87, T88), T7) → U12_ga(T87, T88, T7, transformA_in_ga(T87, T91))
U12_ga(T87, T88, T7, transformA_out_ga(T87, T91)) → U13_ga(T87, T88, T7, cnfequivB_in_ga(o(T91, T88), T7))
cnfequivB_in_ga(o(T213, T214), T7) → U14_ga(T213, T214, T7, transformA_in_ga(T214, X278))
U14_ga(T213, T214, T7, transformA_out_ga(T214, X278)) → cnfequivB_out_ga(o(T213, T214), T7)
cnfequivB_in_ga(o(T213, T214), T7) → U15_ga(T213, T214, T7, transformA_in_ga(T214, T217))
U15_ga(T213, T214, T7, transformA_out_ga(T214, T217)) → U16_ga(T213, T214, T7, cnfequivB_in_ga(o(T213, T217), T7))
cnfequivB_in_ga(a(T231, T232), T7) → U17_ga(T231, T232, T7, transformA_in_ga(T231, X305))
U17_ga(T231, T232, T7, transformA_out_ga(T231, X305)) → cnfequivB_out_ga(a(T231, T232), T7)
cnfequivB_in_ga(a(T231, T232), T7) → U18_ga(T231, T232, T7, transformA_in_ga(T231, T235))
U18_ga(T231, T232, T7, transformA_out_ga(T231, T235)) → U19_ga(T231, T232, T7, cnfequivB_in_ga(a(T235, T232), T7))
cnfequivB_in_ga(a(T249, T250), T7) → U20_ga(T249, T250, T7, transformA_in_ga(T250, X332))
U20_ga(T249, T250, T7, transformA_out_ga(T250, X332)) → cnfequivB_out_ga(a(T249, T250), T7)
cnfequivB_in_ga(a(T249, T250), T7) → U21_ga(T249, T250, T7, transformA_in_ga(T250, T253))
U21_ga(T249, T250, T7, transformA_out_ga(T250, T253)) → U22_ga(T249, T250, T7, cnfequivB_in_ga(a(T249, T253), T7))
cnfequivB_in_ga(n(T263), T7) → U23_ga(T263, T7, transformA_in_ga(T263, X354))
U23_ga(T263, T7, transformA_out_ga(T263, X354)) → cnfequivB_out_ga(n(T263), T7)
cnfequivB_in_ga(n(T263), T7) → U24_ga(T263, T7, transformA_in_ga(T263, T266))
U24_ga(T263, T7, transformA_out_ga(T263, T266)) → U25_ga(T263, T7, cnfequivB_in_ga(n(T266), T7))
cnfequivB_in_ga(T273, T273) → cnfequivB_out_ga(T273, T273)
U25_ga(T263, T7, cnfequivB_out_ga(n(T266), T7)) → cnfequivB_out_ga(n(T263), T7)
U22_ga(T249, T250, T7, cnfequivB_out_ga(a(T249, T253), T7)) → cnfequivB_out_ga(a(T249, T250), T7)
U19_ga(T231, T232, T7, cnfequivB_out_ga(a(T235, T232), T7)) → cnfequivB_out_ga(a(T231, T232), T7)
U16_ga(T213, T214, T7, cnfequivB_out_ga(o(T213, T217), T7)) → cnfequivB_out_ga(o(T213, T214), T7)
U13_ga(T87, T88, T7, cnfequivB_out_ga(o(T91, T88), T7)) → cnfequivB_out_ga(o(T87, T88), T7)
U10_ga(T72, T73, T74, T7, cnfequivB_out_ga(a(o(T72, T74), o(T73, T74)), T7)) → cnfequivB_out_ga(o(a(T72, T73), T74), T7)
U9_ga(T53, T54, T55, T7, cnfequivB_out_ga(a(o(T53, T54), o(T53, T55)), T7)) → cnfequivB_out_ga(o(T53, a(T54, T55)), T7)
U8_ga(T36, T37, T7, cnfequivB_out_ga(a(n(T36), n(T37)), T7)) → cnfequivB_out_ga(n(o(T36, T37)), T7)
U7_ga(T23, T24, T7, cnfequivB_out_ga(o(n(T23), n(T24)), T7)) → cnfequivB_out_ga(n(a(T23, T24)), T7)
U6_ga(T12, T7, cnfequivB_out_ga(T12, T7)) → cnfequivB_out_ga(n(n(T12)), T7)
CNFEQUIVB_IN_GA(a(T231, T232), T7) → U18_GA(T231, T232, T7, transformA_in_ga(T231, T235))
U18_GA(T231, T232, T7, transformA_out_ga(T231, T235)) → CNFEQUIVB_IN_GA(a(T235, T232), T7)
CNFEQUIVB_IN_GA(a(T249, T250), T7) → U21_GA(T249, T250, T7, transformA_in_ga(T250, T253))
U21_GA(T249, T250, T7, transformA_out_ga(T250, T253)) → CNFEQUIVB_IN_GA(a(T249, T253), T7)
transformA_in_ga(n(n(T98)), T98) → transformA_out_ga(n(n(T98)), T98)
transformA_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transformA_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformA_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transformA_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformA_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transformA_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformA_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transformA_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformA_in_ga(o(T157, T158), o(X176, T158)) → U1_ga(T157, T158, X176, transformA_in_ga(T157, X176))
transformA_in_ga(o(T169, T170), o(T169, X198)) → U2_ga(T169, T170, X198, transformA_in_ga(T170, X198))
transformA_in_ga(a(T181, T182), a(X220, T182)) → U3_ga(T181, T182, X220, transformA_in_ga(T181, X220))
transformA_in_ga(a(T193, T194), a(T193, X242)) → U4_ga(T193, T194, X242, transformA_in_ga(T194, X242))
transformA_in_ga(n(T199), n(X253)) → U5_ga(T199, X253, transformA_in_ga(T199, X253))
U1_ga(T157, T158, X176, transformA_out_ga(T157, X176)) → transformA_out_ga(o(T157, T158), o(X176, T158))
U2_ga(T169, T170, X198, transformA_out_ga(T170, X198)) → transformA_out_ga(o(T169, T170), o(T169, X198))
U3_ga(T181, T182, X220, transformA_out_ga(T181, X220)) → transformA_out_ga(a(T181, T182), a(X220, T182))
U4_ga(T193, T194, X242, transformA_out_ga(T194, X242)) → transformA_out_ga(a(T193, T194), a(T193, X242))
U5_ga(T199, X253, transformA_out_ga(T199, X253)) → transformA_out_ga(n(T199), n(X253))
CNFEQUIVB_IN_GA(a(T231, T232)) → U18_GA(T232, transformA_in_ga(T231))
U18_GA(T232, transformA_out_ga(T235)) → CNFEQUIVB_IN_GA(a(T235, T232))
CNFEQUIVB_IN_GA(a(T249, T250)) → U21_GA(T249, transformA_in_ga(T250))
U21_GA(T249, transformA_out_ga(T253)) → CNFEQUIVB_IN_GA(a(T249, T253))
transformA_in_ga(n(n(T98))) → transformA_out_ga(T98)
transformA_in_ga(n(a(T107, T108))) → transformA_out_ga(o(n(T107), n(T108)))
transformA_in_ga(n(o(T117, T118))) → transformA_out_ga(a(n(T117), n(T118)))
transformA_in_ga(o(T131, a(T132, T133))) → transformA_out_ga(a(o(T131, T132), o(T131, T133)))
transformA_in_ga(o(a(T146, T147), T148)) → transformA_out_ga(a(o(T146, T148), o(T147, T148)))
transformA_in_ga(o(T157, T158)) → U1_ga(T158, transformA_in_ga(T157))
transformA_in_ga(o(T169, T170)) → U2_ga(T169, transformA_in_ga(T170))
transformA_in_ga(a(T181, T182)) → U3_ga(T182, transformA_in_ga(T181))
transformA_in_ga(a(T193, T194)) → U4_ga(T193, transformA_in_ga(T194))
transformA_in_ga(n(T199)) → U5_ga(transformA_in_ga(T199))
U1_ga(T158, transformA_out_ga(X176)) → transformA_out_ga(o(X176, T158))
U2_ga(T169, transformA_out_ga(X198)) → transformA_out_ga(o(T169, X198))
U3_ga(T182, transformA_out_ga(X220)) → transformA_out_ga(a(X220, T182))
U4_ga(T193, transformA_out_ga(X242)) → transformA_out_ga(a(T193, X242))
U5_ga(transformA_out_ga(X253)) → transformA_out_ga(n(X253))
transformA_in_ga(x0)
U1_ga(x0, x1)
U2_ga(x0, x1)
U3_ga(x0, x1)
U4_ga(x0, x1)
U5_ga(x0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
CNFEQUIVB_IN_GA(a(T231, T232)) → U18_GA(T232, transformA_in_ga(T231))
U18_GA(T232, transformA_out_ga(T235)) → CNFEQUIVB_IN_GA(a(T235, T232))
CNFEQUIVB_IN_GA(a(T249, T250)) → U21_GA(T249, transformA_in_ga(T250))
U21_GA(T249, transformA_out_ga(T253)) → CNFEQUIVB_IN_GA(a(T249, T253))
[n1, U5ga1] > [o2, U1ga2, U2ga2] > [a2, U18GA2, U21GA2, U3ga2, U4ga2] > transformAoutga1 > CNFEQUIVBINGA1
CNFEQUIVBINGA1: multiset
a2: multiset
U18GA2: multiset
transformAoutga1: [1]
U21GA2: multiset
n1: [1]
o2: [2,1]
U1ga2: [1,2]
U2ga2: [2,1]
U3ga2: multiset
U4ga2: multiset
U5ga1: [1]
transformA_in_ga(n(n(T98))) → transformA_out_ga(T98)
transformA_in_ga(n(a(T107, T108))) → transformA_out_ga(o(n(T107), n(T108)))
transformA_in_ga(n(o(T117, T118))) → transformA_out_ga(a(n(T117), n(T118)))
transformA_in_ga(o(T131, a(T132, T133))) → transformA_out_ga(a(o(T131, T132), o(T131, T133)))
transformA_in_ga(o(a(T146, T147), T148)) → transformA_out_ga(a(o(T146, T148), o(T147, T148)))
transformA_in_ga(o(T157, T158)) → U1_ga(T158, transformA_in_ga(T157))
transformA_in_ga(o(T169, T170)) → U2_ga(T169, transformA_in_ga(T170))
transformA_in_ga(a(T181, T182)) → U3_ga(T182, transformA_in_ga(T181))
transformA_in_ga(a(T193, T194)) → U4_ga(T193, transformA_in_ga(T194))
transformA_in_ga(n(T199)) → U5_ga(transformA_in_ga(T199))
U2_ga(T169, transformA_out_ga(X198)) → transformA_out_ga(o(T169, X198))
U1_ga(T158, transformA_out_ga(X176)) → transformA_out_ga(o(X176, T158))
U3_ga(T182, transformA_out_ga(X220)) → transformA_out_ga(a(X220, T182))
U4_ga(T193, transformA_out_ga(X242)) → transformA_out_ga(a(T193, X242))
U5_ga(transformA_out_ga(X253)) → transformA_out_ga(n(X253))
transformA_in_ga(n(n(T98))) → transformA_out_ga(T98)
transformA_in_ga(n(a(T107, T108))) → transformA_out_ga(o(n(T107), n(T108)))
transformA_in_ga(n(o(T117, T118))) → transformA_out_ga(a(n(T117), n(T118)))
transformA_in_ga(o(T131, a(T132, T133))) → transformA_out_ga(a(o(T131, T132), o(T131, T133)))
transformA_in_ga(o(a(T146, T147), T148)) → transformA_out_ga(a(o(T146, T148), o(T147, T148)))
transformA_in_ga(o(T157, T158)) → U1_ga(T158, transformA_in_ga(T157))
transformA_in_ga(o(T169, T170)) → U2_ga(T169, transformA_in_ga(T170))
transformA_in_ga(a(T181, T182)) → U3_ga(T182, transformA_in_ga(T181))
transformA_in_ga(a(T193, T194)) → U4_ga(T193, transformA_in_ga(T194))
transformA_in_ga(n(T199)) → U5_ga(transformA_in_ga(T199))
U1_ga(T158, transformA_out_ga(X176)) → transformA_out_ga(o(X176, T158))
U2_ga(T169, transformA_out_ga(X198)) → transformA_out_ga(o(T169, X198))
U3_ga(T182, transformA_out_ga(X220)) → transformA_out_ga(a(X220, T182))
U4_ga(T193, transformA_out_ga(X242)) → transformA_out_ga(a(T193, X242))
U5_ga(transformA_out_ga(X253)) → transformA_out_ga(n(X253))
transformA_in_ga(x0)
U1_ga(x0, x1)
U2_ga(x0, x1)
U3_ga(x0, x1)
U4_ga(x0, x1)
U5_ga(x0)
CNFEQUIVB_IN_GA(o(T87, T88), T7) → U12_GA(T87, T88, T7, transformA_in_ga(T87, T91))
U12_GA(T87, T88, T7, transformA_out_ga(T87, T91)) → CNFEQUIVB_IN_GA(o(T91, T88), T7)
CNFEQUIVB_IN_GA(o(T213, T214), T7) → U15_GA(T213, T214, T7, transformA_in_ga(T214, T217))
U15_GA(T213, T214, T7, transformA_out_ga(T214, T217)) → CNFEQUIVB_IN_GA(o(T213, T217), T7)
cnfequivB_in_ga(n(n(T12)), T7) → U6_ga(T12, T7, cnfequivB_in_ga(T12, T7))
cnfequivB_in_ga(n(a(T23, T24)), T7) → U7_ga(T23, T24, T7, cnfequivB_in_ga(o(n(T23), n(T24)), T7))
cnfequivB_in_ga(n(o(T36, T37)), T7) → U8_ga(T36, T37, T7, cnfequivB_in_ga(a(n(T36), n(T37)), T7))
cnfequivB_in_ga(o(T53, a(T54, T55)), T7) → U9_ga(T53, T54, T55, T7, cnfequivB_in_ga(a(o(T53, T54), o(T53, T55)), T7))
cnfequivB_in_ga(o(a(T72, T73), T74), T7) → U10_ga(T72, T73, T74, T7, cnfequivB_in_ga(a(o(T72, T74), o(T73, T74)), T7))
cnfequivB_in_ga(o(T87, T88), T7) → U11_ga(T87, T88, T7, transformA_in_ga(T87, X97))
transformA_in_ga(n(n(T98)), T98) → transformA_out_ga(n(n(T98)), T98)
transformA_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transformA_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformA_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transformA_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformA_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transformA_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformA_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transformA_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformA_in_ga(o(T157, T158), o(X176, T158)) → U1_ga(T157, T158, X176, transformA_in_ga(T157, X176))
transformA_in_ga(o(T169, T170), o(T169, X198)) → U2_ga(T169, T170, X198, transformA_in_ga(T170, X198))
transformA_in_ga(a(T181, T182), a(X220, T182)) → U3_ga(T181, T182, X220, transformA_in_ga(T181, X220))
transformA_in_ga(a(T193, T194), a(T193, X242)) → U4_ga(T193, T194, X242, transformA_in_ga(T194, X242))
transformA_in_ga(n(T199), n(X253)) → U5_ga(T199, X253, transformA_in_ga(T199, X253))
U5_ga(T199, X253, transformA_out_ga(T199, X253)) → transformA_out_ga(n(T199), n(X253))
U4_ga(T193, T194, X242, transformA_out_ga(T194, X242)) → transformA_out_ga(a(T193, T194), a(T193, X242))
U3_ga(T181, T182, X220, transformA_out_ga(T181, X220)) → transformA_out_ga(a(T181, T182), a(X220, T182))
U2_ga(T169, T170, X198, transformA_out_ga(T170, X198)) → transformA_out_ga(o(T169, T170), o(T169, X198))
U1_ga(T157, T158, X176, transformA_out_ga(T157, X176)) → transformA_out_ga(o(T157, T158), o(X176, T158))
U11_ga(T87, T88, T7, transformA_out_ga(T87, X97)) → cnfequivB_out_ga(o(T87, T88), T7)
cnfequivB_in_ga(o(T87, T88), T7) → U12_ga(T87, T88, T7, transformA_in_ga(T87, T91))
U12_ga(T87, T88, T7, transformA_out_ga(T87, T91)) → U13_ga(T87, T88, T7, cnfequivB_in_ga(o(T91, T88), T7))
cnfequivB_in_ga(o(T213, T214), T7) → U14_ga(T213, T214, T7, transformA_in_ga(T214, X278))
U14_ga(T213, T214, T7, transformA_out_ga(T214, X278)) → cnfequivB_out_ga(o(T213, T214), T7)
cnfequivB_in_ga(o(T213, T214), T7) → U15_ga(T213, T214, T7, transformA_in_ga(T214, T217))
U15_ga(T213, T214, T7, transformA_out_ga(T214, T217)) → U16_ga(T213, T214, T7, cnfequivB_in_ga(o(T213, T217), T7))
cnfequivB_in_ga(a(T231, T232), T7) → U17_ga(T231, T232, T7, transformA_in_ga(T231, X305))
U17_ga(T231, T232, T7, transformA_out_ga(T231, X305)) → cnfequivB_out_ga(a(T231, T232), T7)
cnfequivB_in_ga(a(T231, T232), T7) → U18_ga(T231, T232, T7, transformA_in_ga(T231, T235))
U18_ga(T231, T232, T7, transformA_out_ga(T231, T235)) → U19_ga(T231, T232, T7, cnfequivB_in_ga(a(T235, T232), T7))
cnfequivB_in_ga(a(T249, T250), T7) → U20_ga(T249, T250, T7, transformA_in_ga(T250, X332))
U20_ga(T249, T250, T7, transformA_out_ga(T250, X332)) → cnfequivB_out_ga(a(T249, T250), T7)
cnfequivB_in_ga(a(T249, T250), T7) → U21_ga(T249, T250, T7, transformA_in_ga(T250, T253))
U21_ga(T249, T250, T7, transformA_out_ga(T250, T253)) → U22_ga(T249, T250, T7, cnfequivB_in_ga(a(T249, T253), T7))
cnfequivB_in_ga(n(T263), T7) → U23_ga(T263, T7, transformA_in_ga(T263, X354))
U23_ga(T263, T7, transformA_out_ga(T263, X354)) → cnfequivB_out_ga(n(T263), T7)
cnfequivB_in_ga(n(T263), T7) → U24_ga(T263, T7, transformA_in_ga(T263, T266))
U24_ga(T263, T7, transformA_out_ga(T263, T266)) → U25_ga(T263, T7, cnfequivB_in_ga(n(T266), T7))
cnfequivB_in_ga(T273, T273) → cnfequivB_out_ga(T273, T273)
U25_ga(T263, T7, cnfequivB_out_ga(n(T266), T7)) → cnfequivB_out_ga(n(T263), T7)
U22_ga(T249, T250, T7, cnfequivB_out_ga(a(T249, T253), T7)) → cnfequivB_out_ga(a(T249, T250), T7)
U19_ga(T231, T232, T7, cnfequivB_out_ga(a(T235, T232), T7)) → cnfequivB_out_ga(a(T231, T232), T7)
U16_ga(T213, T214, T7, cnfequivB_out_ga(o(T213, T217), T7)) → cnfequivB_out_ga(o(T213, T214), T7)
U13_ga(T87, T88, T7, cnfequivB_out_ga(o(T91, T88), T7)) → cnfequivB_out_ga(o(T87, T88), T7)
U10_ga(T72, T73, T74, T7, cnfequivB_out_ga(a(o(T72, T74), o(T73, T74)), T7)) → cnfequivB_out_ga(o(a(T72, T73), T74), T7)
U9_ga(T53, T54, T55, T7, cnfequivB_out_ga(a(o(T53, T54), o(T53, T55)), T7)) → cnfequivB_out_ga(o(T53, a(T54, T55)), T7)
U8_ga(T36, T37, T7, cnfequivB_out_ga(a(n(T36), n(T37)), T7)) → cnfequivB_out_ga(n(o(T36, T37)), T7)
U7_ga(T23, T24, T7, cnfequivB_out_ga(o(n(T23), n(T24)), T7)) → cnfequivB_out_ga(n(a(T23, T24)), T7)
U6_ga(T12, T7, cnfequivB_out_ga(T12, T7)) → cnfequivB_out_ga(n(n(T12)), T7)
CNFEQUIVB_IN_GA(o(T87, T88), T7) → U12_GA(T87, T88, T7, transformA_in_ga(T87, T91))
U12_GA(T87, T88, T7, transformA_out_ga(T87, T91)) → CNFEQUIVB_IN_GA(o(T91, T88), T7)
CNFEQUIVB_IN_GA(o(T213, T214), T7) → U15_GA(T213, T214, T7, transformA_in_ga(T214, T217))
U15_GA(T213, T214, T7, transformA_out_ga(T214, T217)) → CNFEQUIVB_IN_GA(o(T213, T217), T7)
transformA_in_ga(n(n(T98)), T98) → transformA_out_ga(n(n(T98)), T98)
transformA_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transformA_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformA_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transformA_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformA_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transformA_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformA_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transformA_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformA_in_ga(o(T157, T158), o(X176, T158)) → U1_ga(T157, T158, X176, transformA_in_ga(T157, X176))
transformA_in_ga(o(T169, T170), o(T169, X198)) → U2_ga(T169, T170, X198, transformA_in_ga(T170, X198))
transformA_in_ga(a(T181, T182), a(X220, T182)) → U3_ga(T181, T182, X220, transformA_in_ga(T181, X220))
transformA_in_ga(a(T193, T194), a(T193, X242)) → U4_ga(T193, T194, X242, transformA_in_ga(T194, X242))
transformA_in_ga(n(T199), n(X253)) → U5_ga(T199, X253, transformA_in_ga(T199, X253))
U1_ga(T157, T158, X176, transformA_out_ga(T157, X176)) → transformA_out_ga(o(T157, T158), o(X176, T158))
U2_ga(T169, T170, X198, transformA_out_ga(T170, X198)) → transformA_out_ga(o(T169, T170), o(T169, X198))
U3_ga(T181, T182, X220, transformA_out_ga(T181, X220)) → transformA_out_ga(a(T181, T182), a(X220, T182))
U4_ga(T193, T194, X242, transformA_out_ga(T194, X242)) → transformA_out_ga(a(T193, T194), a(T193, X242))
U5_ga(T199, X253, transformA_out_ga(T199, X253)) → transformA_out_ga(n(T199), n(X253))
CNFEQUIVB_IN_GA(o(T87, T88)) → U12_GA(T88, transformA_in_ga(T87))
U12_GA(T88, transformA_out_ga(T91)) → CNFEQUIVB_IN_GA(o(T91, T88))
CNFEQUIVB_IN_GA(o(T213, T214)) → U15_GA(T213, transformA_in_ga(T214))
U15_GA(T213, transformA_out_ga(T217)) → CNFEQUIVB_IN_GA(o(T213, T217))
transformA_in_ga(n(n(T98))) → transformA_out_ga(T98)
transformA_in_ga(n(a(T107, T108))) → transformA_out_ga(o(n(T107), n(T108)))
transformA_in_ga(n(o(T117, T118))) → transformA_out_ga(a(n(T117), n(T118)))
transformA_in_ga(o(T131, a(T132, T133))) → transformA_out_ga(a(o(T131, T132), o(T131, T133)))
transformA_in_ga(o(a(T146, T147), T148)) → transformA_out_ga(a(o(T146, T148), o(T147, T148)))
transformA_in_ga(o(T157, T158)) → U1_ga(T158, transformA_in_ga(T157))
transformA_in_ga(o(T169, T170)) → U2_ga(T169, transformA_in_ga(T170))
transformA_in_ga(a(T181, T182)) → U3_ga(T182, transformA_in_ga(T181))
transformA_in_ga(a(T193, T194)) → U4_ga(T193, transformA_in_ga(T194))
transformA_in_ga(n(T199)) → U5_ga(transformA_in_ga(T199))
U1_ga(T158, transformA_out_ga(X176)) → transformA_out_ga(o(X176, T158))
U2_ga(T169, transformA_out_ga(X198)) → transformA_out_ga(o(T169, X198))
U3_ga(T182, transformA_out_ga(X220)) → transformA_out_ga(a(X220, T182))
U4_ga(T193, transformA_out_ga(X242)) → transformA_out_ga(a(T193, X242))
U5_ga(transformA_out_ga(X253)) → transformA_out_ga(n(X253))
transformA_in_ga(x0)
U1_ga(x0, x1)
U2_ga(x0, x1)
U3_ga(x0, x1)
U4_ga(x0, x1)
U5_ga(x0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U12_GA(T88, transformA_out_ga(T91)) → CNFEQUIVB_IN_GA(o(T91, T88))
U15_GA(T213, transformA_out_ga(T217)) → CNFEQUIVB_IN_GA(o(T213, T217))
[n1, U5ga1] > [o2, U12GA2, U15GA2, U1ga2, U2ga2] > [a2, U3ga2, U4ga2] > transformAoutga1
o2: multiset
U12GA2: multiset
transformAoutga1: multiset
U15GA2: multiset
n1: [1]
a2: multiset
U1ga2: multiset
U2ga2: multiset
U3ga2: multiset
U4ga2: multiset
U5ga1: [1]
transformA_in_ga(n(n(T98))) → transformA_out_ga(T98)
transformA_in_ga(n(a(T107, T108))) → transformA_out_ga(o(n(T107), n(T108)))
transformA_in_ga(n(o(T117, T118))) → transformA_out_ga(a(n(T117), n(T118)))
transformA_in_ga(o(T131, a(T132, T133))) → transformA_out_ga(a(o(T131, T132), o(T131, T133)))
transformA_in_ga(o(a(T146, T147), T148)) → transformA_out_ga(a(o(T146, T148), o(T147, T148)))
transformA_in_ga(o(T157, T158)) → U1_ga(T158, transformA_in_ga(T157))
transformA_in_ga(o(T169, T170)) → U2_ga(T169, transformA_in_ga(T170))
transformA_in_ga(a(T181, T182)) → U3_ga(T182, transformA_in_ga(T181))
transformA_in_ga(a(T193, T194)) → U4_ga(T193, transformA_in_ga(T194))
transformA_in_ga(n(T199)) → U5_ga(transformA_in_ga(T199))
U2_ga(T169, transformA_out_ga(X198)) → transformA_out_ga(o(T169, X198))
U1_ga(T158, transformA_out_ga(X176)) → transformA_out_ga(o(X176, T158))
U3_ga(T182, transformA_out_ga(X220)) → transformA_out_ga(a(X220, T182))
U4_ga(T193, transformA_out_ga(X242)) → transformA_out_ga(a(T193, X242))
U5_ga(transformA_out_ga(X253)) → transformA_out_ga(n(X253))
CNFEQUIVB_IN_GA(o(T87, T88)) → U12_GA(T88, transformA_in_ga(T87))
CNFEQUIVB_IN_GA(o(T213, T214)) → U15_GA(T213, transformA_in_ga(T214))
transformA_in_ga(n(n(T98))) → transformA_out_ga(T98)
transformA_in_ga(n(a(T107, T108))) → transformA_out_ga(o(n(T107), n(T108)))
transformA_in_ga(n(o(T117, T118))) → transformA_out_ga(a(n(T117), n(T118)))
transformA_in_ga(o(T131, a(T132, T133))) → transformA_out_ga(a(o(T131, T132), o(T131, T133)))
transformA_in_ga(o(a(T146, T147), T148)) → transformA_out_ga(a(o(T146, T148), o(T147, T148)))
transformA_in_ga(o(T157, T158)) → U1_ga(T158, transformA_in_ga(T157))
transformA_in_ga(o(T169, T170)) → U2_ga(T169, transformA_in_ga(T170))
transformA_in_ga(a(T181, T182)) → U3_ga(T182, transformA_in_ga(T181))
transformA_in_ga(a(T193, T194)) → U4_ga(T193, transformA_in_ga(T194))
transformA_in_ga(n(T199)) → U5_ga(transformA_in_ga(T199))
U1_ga(T158, transformA_out_ga(X176)) → transformA_out_ga(o(X176, T158))
U2_ga(T169, transformA_out_ga(X198)) → transformA_out_ga(o(T169, X198))
U3_ga(T182, transformA_out_ga(X220)) → transformA_out_ga(a(X220, T182))
U4_ga(T193, transformA_out_ga(X242)) → transformA_out_ga(a(T193, X242))
U5_ga(transformA_out_ga(X253)) → transformA_out_ga(n(X253))
transformA_in_ga(x0)
U1_ga(x0, x1)
U2_ga(x0, x1)
U3_ga(x0, x1)
U4_ga(x0, x1)
U5_ga(x0)
CNFEQUIVB_IN_GA(n(T263), T7) → U24_GA(T263, T7, transformA_in_ga(T263, T266))
U24_GA(T263, T7, transformA_out_ga(T263, T266)) → CNFEQUIVB_IN_GA(n(T266), T7)
CNFEQUIVB_IN_GA(n(n(T12)), T7) → CNFEQUIVB_IN_GA(T12, T7)
cnfequivB_in_ga(n(n(T12)), T7) → U6_ga(T12, T7, cnfequivB_in_ga(T12, T7))
cnfequivB_in_ga(n(a(T23, T24)), T7) → U7_ga(T23, T24, T7, cnfequivB_in_ga(o(n(T23), n(T24)), T7))
cnfequivB_in_ga(n(o(T36, T37)), T7) → U8_ga(T36, T37, T7, cnfequivB_in_ga(a(n(T36), n(T37)), T7))
cnfequivB_in_ga(o(T53, a(T54, T55)), T7) → U9_ga(T53, T54, T55, T7, cnfequivB_in_ga(a(o(T53, T54), o(T53, T55)), T7))
cnfequivB_in_ga(o(a(T72, T73), T74), T7) → U10_ga(T72, T73, T74, T7, cnfequivB_in_ga(a(o(T72, T74), o(T73, T74)), T7))
cnfequivB_in_ga(o(T87, T88), T7) → U11_ga(T87, T88, T7, transformA_in_ga(T87, X97))
transformA_in_ga(n(n(T98)), T98) → transformA_out_ga(n(n(T98)), T98)
transformA_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transformA_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformA_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transformA_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformA_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transformA_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformA_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transformA_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformA_in_ga(o(T157, T158), o(X176, T158)) → U1_ga(T157, T158, X176, transformA_in_ga(T157, X176))
transformA_in_ga(o(T169, T170), o(T169, X198)) → U2_ga(T169, T170, X198, transformA_in_ga(T170, X198))
transformA_in_ga(a(T181, T182), a(X220, T182)) → U3_ga(T181, T182, X220, transformA_in_ga(T181, X220))
transformA_in_ga(a(T193, T194), a(T193, X242)) → U4_ga(T193, T194, X242, transformA_in_ga(T194, X242))
transformA_in_ga(n(T199), n(X253)) → U5_ga(T199, X253, transformA_in_ga(T199, X253))
U5_ga(T199, X253, transformA_out_ga(T199, X253)) → transformA_out_ga(n(T199), n(X253))
U4_ga(T193, T194, X242, transformA_out_ga(T194, X242)) → transformA_out_ga(a(T193, T194), a(T193, X242))
U3_ga(T181, T182, X220, transformA_out_ga(T181, X220)) → transformA_out_ga(a(T181, T182), a(X220, T182))
U2_ga(T169, T170, X198, transformA_out_ga(T170, X198)) → transformA_out_ga(o(T169, T170), o(T169, X198))
U1_ga(T157, T158, X176, transformA_out_ga(T157, X176)) → transformA_out_ga(o(T157, T158), o(X176, T158))
U11_ga(T87, T88, T7, transformA_out_ga(T87, X97)) → cnfequivB_out_ga(o(T87, T88), T7)
cnfequivB_in_ga(o(T87, T88), T7) → U12_ga(T87, T88, T7, transformA_in_ga(T87, T91))
U12_ga(T87, T88, T7, transformA_out_ga(T87, T91)) → U13_ga(T87, T88, T7, cnfequivB_in_ga(o(T91, T88), T7))
cnfequivB_in_ga(o(T213, T214), T7) → U14_ga(T213, T214, T7, transformA_in_ga(T214, X278))
U14_ga(T213, T214, T7, transformA_out_ga(T214, X278)) → cnfequivB_out_ga(o(T213, T214), T7)
cnfequivB_in_ga(o(T213, T214), T7) → U15_ga(T213, T214, T7, transformA_in_ga(T214, T217))
U15_ga(T213, T214, T7, transformA_out_ga(T214, T217)) → U16_ga(T213, T214, T7, cnfequivB_in_ga(o(T213, T217), T7))
cnfequivB_in_ga(a(T231, T232), T7) → U17_ga(T231, T232, T7, transformA_in_ga(T231, X305))
U17_ga(T231, T232, T7, transformA_out_ga(T231, X305)) → cnfequivB_out_ga(a(T231, T232), T7)
cnfequivB_in_ga(a(T231, T232), T7) → U18_ga(T231, T232, T7, transformA_in_ga(T231, T235))
U18_ga(T231, T232, T7, transformA_out_ga(T231, T235)) → U19_ga(T231, T232, T7, cnfequivB_in_ga(a(T235, T232), T7))
cnfequivB_in_ga(a(T249, T250), T7) → U20_ga(T249, T250, T7, transformA_in_ga(T250, X332))
U20_ga(T249, T250, T7, transformA_out_ga(T250, X332)) → cnfequivB_out_ga(a(T249, T250), T7)
cnfequivB_in_ga(a(T249, T250), T7) → U21_ga(T249, T250, T7, transformA_in_ga(T250, T253))
U21_ga(T249, T250, T7, transformA_out_ga(T250, T253)) → U22_ga(T249, T250, T7, cnfequivB_in_ga(a(T249, T253), T7))
cnfequivB_in_ga(n(T263), T7) → U23_ga(T263, T7, transformA_in_ga(T263, X354))
U23_ga(T263, T7, transformA_out_ga(T263, X354)) → cnfequivB_out_ga(n(T263), T7)
cnfequivB_in_ga(n(T263), T7) → U24_ga(T263, T7, transformA_in_ga(T263, T266))
U24_ga(T263, T7, transformA_out_ga(T263, T266)) → U25_ga(T263, T7, cnfequivB_in_ga(n(T266), T7))
cnfequivB_in_ga(T273, T273) → cnfequivB_out_ga(T273, T273)
U25_ga(T263, T7, cnfequivB_out_ga(n(T266), T7)) → cnfequivB_out_ga(n(T263), T7)
U22_ga(T249, T250, T7, cnfequivB_out_ga(a(T249, T253), T7)) → cnfequivB_out_ga(a(T249, T250), T7)
U19_ga(T231, T232, T7, cnfequivB_out_ga(a(T235, T232), T7)) → cnfequivB_out_ga(a(T231, T232), T7)
U16_ga(T213, T214, T7, cnfequivB_out_ga(o(T213, T217), T7)) → cnfequivB_out_ga(o(T213, T214), T7)
U13_ga(T87, T88, T7, cnfequivB_out_ga(o(T91, T88), T7)) → cnfequivB_out_ga(o(T87, T88), T7)
U10_ga(T72, T73, T74, T7, cnfequivB_out_ga(a(o(T72, T74), o(T73, T74)), T7)) → cnfequivB_out_ga(o(a(T72, T73), T74), T7)
U9_ga(T53, T54, T55, T7, cnfequivB_out_ga(a(o(T53, T54), o(T53, T55)), T7)) → cnfequivB_out_ga(o(T53, a(T54, T55)), T7)
U8_ga(T36, T37, T7, cnfequivB_out_ga(a(n(T36), n(T37)), T7)) → cnfequivB_out_ga(n(o(T36, T37)), T7)
U7_ga(T23, T24, T7, cnfequivB_out_ga(o(n(T23), n(T24)), T7)) → cnfequivB_out_ga(n(a(T23, T24)), T7)
U6_ga(T12, T7, cnfequivB_out_ga(T12, T7)) → cnfequivB_out_ga(n(n(T12)), T7)
CNFEQUIVB_IN_GA(n(T263), T7) → U24_GA(T263, T7, transformA_in_ga(T263, T266))
U24_GA(T263, T7, transformA_out_ga(T263, T266)) → CNFEQUIVB_IN_GA(n(T266), T7)
CNFEQUIVB_IN_GA(n(n(T12)), T7) → CNFEQUIVB_IN_GA(T12, T7)
transformA_in_ga(n(n(T98)), T98) → transformA_out_ga(n(n(T98)), T98)
transformA_in_ga(n(a(T107, T108)), o(n(T107), n(T108))) → transformA_out_ga(n(a(T107, T108)), o(n(T107), n(T108)))
transformA_in_ga(n(o(T117, T118)), a(n(T117), n(T118))) → transformA_out_ga(n(o(T117, T118)), a(n(T117), n(T118)))
transformA_in_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133))) → transformA_out_ga(o(T131, a(T132, T133)), a(o(T131, T132), o(T131, T133)))
transformA_in_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148))) → transformA_out_ga(o(a(T146, T147), T148), a(o(T146, T148), o(T147, T148)))
transformA_in_ga(o(T157, T158), o(X176, T158)) → U1_ga(T157, T158, X176, transformA_in_ga(T157, X176))
transformA_in_ga(o(T169, T170), o(T169, X198)) → U2_ga(T169, T170, X198, transformA_in_ga(T170, X198))
transformA_in_ga(a(T181, T182), a(X220, T182)) → U3_ga(T181, T182, X220, transformA_in_ga(T181, X220))
transformA_in_ga(a(T193, T194), a(T193, X242)) → U4_ga(T193, T194, X242, transformA_in_ga(T194, X242))
transformA_in_ga(n(T199), n(X253)) → U5_ga(T199, X253, transformA_in_ga(T199, X253))
U1_ga(T157, T158, X176, transformA_out_ga(T157, X176)) → transformA_out_ga(o(T157, T158), o(X176, T158))
U2_ga(T169, T170, X198, transformA_out_ga(T170, X198)) → transformA_out_ga(o(T169, T170), o(T169, X198))
U3_ga(T181, T182, X220, transformA_out_ga(T181, X220)) → transformA_out_ga(a(T181, T182), a(X220, T182))
U4_ga(T193, T194, X242, transformA_out_ga(T194, X242)) → transformA_out_ga(a(T193, T194), a(T193, X242))
U5_ga(T199, X253, transformA_out_ga(T199, X253)) → transformA_out_ga(n(T199), n(X253))
CNFEQUIVB_IN_GA(n(T263)) → U24_GA(transformA_in_ga(T263))
U24_GA(transformA_out_ga(T266)) → CNFEQUIVB_IN_GA(n(T266))
CNFEQUIVB_IN_GA(n(n(T12))) → CNFEQUIVB_IN_GA(T12)
transformA_in_ga(n(n(T98))) → transformA_out_ga(T98)
transformA_in_ga(n(a(T107, T108))) → transformA_out_ga(o(n(T107), n(T108)))
transformA_in_ga(n(o(T117, T118))) → transformA_out_ga(a(n(T117), n(T118)))
transformA_in_ga(o(T131, a(T132, T133))) → transformA_out_ga(a(o(T131, T132), o(T131, T133)))
transformA_in_ga(o(a(T146, T147), T148)) → transformA_out_ga(a(o(T146, T148), o(T147, T148)))
transformA_in_ga(o(T157, T158)) → U1_ga(T158, transformA_in_ga(T157))
transformA_in_ga(o(T169, T170)) → U2_ga(T169, transformA_in_ga(T170))
transformA_in_ga(a(T181, T182)) → U3_ga(T182, transformA_in_ga(T181))
transformA_in_ga(a(T193, T194)) → U4_ga(T193, transformA_in_ga(T194))
transformA_in_ga(n(T199)) → U5_ga(transformA_in_ga(T199))
U1_ga(T158, transformA_out_ga(X176)) → transformA_out_ga(o(X176, T158))
U2_ga(T169, transformA_out_ga(X198)) → transformA_out_ga(o(T169, X198))
U3_ga(T182, transformA_out_ga(X220)) → transformA_out_ga(a(X220, T182))
U4_ga(T193, transformA_out_ga(X242)) → transformA_out_ga(a(T193, X242))
U5_ga(transformA_out_ga(X253)) → transformA_out_ga(n(X253))
transformA_in_ga(x0)
U1_ga(x0, x1)
U2_ga(x0, x1)
U3_ga(x0, x1)
U4_ga(x0, x1)
U5_ga(x0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
CNFEQUIVB_IN_GA(n(n(T12))) → CNFEQUIVB_IN_GA(T12)
POL(CNFEQUIVB_IN_GA(x1)) = x1
POL(U1_ga(x1, x2)) = 0
POL(U24_GA(x1)) = 1 + x1
POL(U2_ga(x1, x2)) = 0
POL(U3_ga(x1, x2)) = 0
POL(U4_ga(x1, x2)) = 0
POL(U5_ga(x1)) = 1 + x1
POL(a(x1, x2)) = 0
POL(n(x1)) = 1 + x1
POL(o(x1, x2)) = 0
POL(transformA_in_ga(x1)) = x1
POL(transformA_out_ga(x1)) = x1
transformA_in_ga(n(n(T98))) → transformA_out_ga(T98)
transformA_in_ga(n(a(T107, T108))) → transformA_out_ga(o(n(T107), n(T108)))
transformA_in_ga(n(o(T117, T118))) → transformA_out_ga(a(n(T117), n(T118)))
transformA_in_ga(o(T131, a(T132, T133))) → transformA_out_ga(a(o(T131, T132), o(T131, T133)))
transformA_in_ga(o(a(T146, T147), T148)) → transformA_out_ga(a(o(T146, T148), o(T147, T148)))
transformA_in_ga(o(T157, T158)) → U1_ga(T158, transformA_in_ga(T157))
transformA_in_ga(o(T169, T170)) → U2_ga(T169, transformA_in_ga(T170))
transformA_in_ga(a(T181, T182)) → U3_ga(T182, transformA_in_ga(T181))
transformA_in_ga(a(T193, T194)) → U4_ga(T193, transformA_in_ga(T194))
transformA_in_ga(n(T199)) → U5_ga(transformA_in_ga(T199))
U2_ga(T169, transformA_out_ga(X198)) → transformA_out_ga(o(T169, X198))
U1_ga(T158, transformA_out_ga(X176)) → transformA_out_ga(o(X176, T158))
U3_ga(T182, transformA_out_ga(X220)) → transformA_out_ga(a(X220, T182))
U4_ga(T193, transformA_out_ga(X242)) → transformA_out_ga(a(T193, X242))
U5_ga(transformA_out_ga(X253)) → transformA_out_ga(n(X253))
CNFEQUIVB_IN_GA(n(T263)) → U24_GA(transformA_in_ga(T263))
U24_GA(transformA_out_ga(T266)) → CNFEQUIVB_IN_GA(n(T266))
transformA_in_ga(n(n(T98))) → transformA_out_ga(T98)
transformA_in_ga(n(a(T107, T108))) → transformA_out_ga(o(n(T107), n(T108)))
transformA_in_ga(n(o(T117, T118))) → transformA_out_ga(a(n(T117), n(T118)))
transformA_in_ga(o(T131, a(T132, T133))) → transformA_out_ga(a(o(T131, T132), o(T131, T133)))
transformA_in_ga(o(a(T146, T147), T148)) → transformA_out_ga(a(o(T146, T148), o(T147, T148)))
transformA_in_ga(o(T157, T158)) → U1_ga(T158, transformA_in_ga(T157))
transformA_in_ga(o(T169, T170)) → U2_ga(T169, transformA_in_ga(T170))
transformA_in_ga(a(T181, T182)) → U3_ga(T182, transformA_in_ga(T181))
transformA_in_ga(a(T193, T194)) → U4_ga(T193, transformA_in_ga(T194))
transformA_in_ga(n(T199)) → U5_ga(transformA_in_ga(T199))
U1_ga(T158, transformA_out_ga(X176)) → transformA_out_ga(o(X176, T158))
U2_ga(T169, transformA_out_ga(X198)) → transformA_out_ga(o(T169, X198))
U3_ga(T182, transformA_out_ga(X220)) → transformA_out_ga(a(X220, T182))
U4_ga(T193, transformA_out_ga(X242)) → transformA_out_ga(a(T193, X242))
U5_ga(transformA_out_ga(X253)) → transformA_out_ga(n(X253))
transformA_in_ga(x0)
U1_ga(x0, x1)
U2_ga(x0, x1)
U3_ga(x0, x1)
U4_ga(x0, x1)
U5_ga(x0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
CNFEQUIVB_IN_GA(n(T263)) → U24_GA(transformA_in_ga(T263))
U24_GA(transformA_out_ga(T266)) → CNFEQUIVB_IN_GA(n(T266))
[n1, U24GA1, U5ga1] > [o2, U1ga2, U2ga2] > [a2, U3ga2, U4ga2] > [CNFEQUIVBINGA1, transformAoutga1]
CNFEQUIVBINGA1: multiset
n1: [1]
U24GA1: [1]
transformAoutga1: multiset
a2: multiset
o2: [2,1]
U1ga2: [1,2]
U2ga2: [2,1]
U3ga2: multiset
U4ga2: multiset
U5ga1: [1]
transformA_in_ga(n(n(T98))) → transformA_out_ga(T98)
transformA_in_ga(n(a(T107, T108))) → transformA_out_ga(o(n(T107), n(T108)))
transformA_in_ga(n(o(T117, T118))) → transformA_out_ga(a(n(T117), n(T118)))
transformA_in_ga(o(T131, a(T132, T133))) → transformA_out_ga(a(o(T131, T132), o(T131, T133)))
transformA_in_ga(o(a(T146, T147), T148)) → transformA_out_ga(a(o(T146, T148), o(T147, T148)))
transformA_in_ga(o(T157, T158)) → U1_ga(T158, transformA_in_ga(T157))
transformA_in_ga(o(T169, T170)) → U2_ga(T169, transformA_in_ga(T170))
transformA_in_ga(a(T181, T182)) → U3_ga(T182, transformA_in_ga(T181))
transformA_in_ga(a(T193, T194)) → U4_ga(T193, transformA_in_ga(T194))
transformA_in_ga(n(T199)) → U5_ga(transformA_in_ga(T199))
U2_ga(T169, transformA_out_ga(X198)) → transformA_out_ga(o(T169, X198))
U1_ga(T158, transformA_out_ga(X176)) → transformA_out_ga(o(X176, T158))
U3_ga(T182, transformA_out_ga(X220)) → transformA_out_ga(a(X220, T182))
U4_ga(T193, transformA_out_ga(X242)) → transformA_out_ga(a(T193, X242))
U5_ga(transformA_out_ga(X253)) → transformA_out_ga(n(X253))
transformA_in_ga(n(n(T98))) → transformA_out_ga(T98)
transformA_in_ga(n(a(T107, T108))) → transformA_out_ga(o(n(T107), n(T108)))
transformA_in_ga(n(o(T117, T118))) → transformA_out_ga(a(n(T117), n(T118)))
transformA_in_ga(o(T131, a(T132, T133))) → transformA_out_ga(a(o(T131, T132), o(T131, T133)))
transformA_in_ga(o(a(T146, T147), T148)) → transformA_out_ga(a(o(T146, T148), o(T147, T148)))
transformA_in_ga(o(T157, T158)) → U1_ga(T158, transformA_in_ga(T157))
transformA_in_ga(o(T169, T170)) → U2_ga(T169, transformA_in_ga(T170))
transformA_in_ga(a(T181, T182)) → U3_ga(T182, transformA_in_ga(T181))
transformA_in_ga(a(T193, T194)) → U4_ga(T193, transformA_in_ga(T194))
transformA_in_ga(n(T199)) → U5_ga(transformA_in_ga(T199))
U1_ga(T158, transformA_out_ga(X176)) → transformA_out_ga(o(X176, T158))
U2_ga(T169, transformA_out_ga(X198)) → transformA_out_ga(o(T169, X198))
U3_ga(T182, transformA_out_ga(X220)) → transformA_out_ga(a(X220, T182))
U4_ga(T193, transformA_out_ga(X242)) → transformA_out_ga(a(T193, X242))
U5_ga(transformA_out_ga(X253)) → transformA_out_ga(n(X253))
transformA_in_ga(x0)
U1_ga(x0, x1)
U2_ga(x0, x1)
U3_ga(x0, x1)
U4_ga(x0, x1)
U5_ga(x0)